Theorem eceqopreq 4297

Description: Equality of equivalence relation in terms of an operation.

Hypotheses

Ref	Expression
eceqopreq.2	|- B e. V
eceqopreq.3	|- C e. V
eceqopreq.4	|- D e. V
eceqopreq.5	|- Er R
eceqopreq.6	|- dom R = (S X. S)
eceqopreq.7	|- dom F = (S X. S)
eceqopreq.8	|- -. (/) e. S
eceqopreq.9	|- ((x e. S /\ y e. S) -> (xFy) e. S)
eceqopreq.10	|- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (<.A, B>.R<.C, D>. <-> (AFD) = (BFC)))

Assertion

Ref	Expression
eceqopreq	|- ((A e. S /\ C e. S) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))

Distinct variable groups:   x,y,F   x,S,y   x,A,y   x,B,y   x,C,y   x,D,y

Proof of Theorem eceqopreq

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . . . . . . . 10 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (A e. S /\ B e. S))
2		opelxpi 3207	. . . . . . . . . . 11 |- ((A e. S /\ B e. S) -> <.A, B>. e. (S X. S))
3		eceqopreq.6	. . . . . . . . . . 11 |- dom R = (S X. S)
4	2, 3	syl6eleqr 1551	. . . . . . . . . 10 |- ((A e. S /\ B e. S) -> <.A, B>. e. dom R)
5		opex 2772	. . . . . . . . . . 11 |- <.C, D>. e. V
6		eceqopreq.5	. . . . . . . . . . 11 |- Er R
7	5, 6	erthdm 4267	. . . . . . . . . 10 |- (<.A, B>. e. dom R -> ([<.A, B>.]R = [<.C, D>.]R <-> <.A, B>.R<.C, D>.))
8	1, 4, 7	3syl 20	. . . . . . . . 9 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]R = [<.C, D>.]R <-> <.A, B>.R<.C, D>.))
9		eceqopreq.10	. . . . . . . . 9 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (<.A, B>.R<.C, D>. <-> (AFD) = (BFC)))
10	8, 9	bitrd 526	. . . . . . . 8 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))
11	10	exp43 384	. . . . . . 7 |- (A e. S -> (B e. S -> (C e. S -> (D e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))))
12	11	3imp 825	. . . . . 6 |- ((A e. S /\ B e. S /\ C e. S) -> (D e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))
13		eqeq1 1473	. . . . . . . . . . . . . 14 |- ([<.A, B>.]R = [<.C, D>.]R -> ([<.A, B>.]R = (/) <-> [<.C, D>.]R = (/)))
14	13	biimprcd 156	. . . . . . . . . . . . 13 |- ([<.C, D>.]R = (/) -> ([<.A, B>.]R = [<.C, D>.]R -> [<.A, B>.]R = (/)))
15	14	con3d 95	. . . . . . . . . . . 12 |- ([<.C, D>.]R = (/) -> (-. [<.A, B>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
16	3	eleq2i 1530	. . . . . . . . . . . . . 14 |- (<.C, D>. e. dom R <-> <.C, D>. e. (S X. S))
17	5	ecdmn0 4264	. . . . . . . . . . . . . 14 |- (<.C, D>. e. dom R <-> -. [<.C, D>.]R = (/))
18		eceqopreq.4	. . . . . . . . . . . . . . 15 |- D e. V
19	18	opelxp 3204	. . . . . . . . . . . . . 14 |- (<.C, D>. e. (S X. S) <-> (C e. S /\ D e. S))
20	16, 17, 19	3bitr3 181	. . . . . . . . . . . . 13 |- (-. [<.C, D>.]R = (/) <-> (C e. S /\ D e. S))
21	20	pm3.27bi 326	. . . . . . . . . . . 12 |- (-. [<.C, D>.]R = (/) -> D e. S)
22	15, 21	nsyl4 120	. . . . . . . . . . 11 |- (-. D e. S -> (-. [<.A, B>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
23	3	eleq2i 1530	. . . . . . . . . . . 12 |- (<.A, B>. e. dom R <-> <.A, B>. e. (S X. S))
24		opex 2772	. . . . . . . . . . . . 13 |- <.A, B>. e. V
25	24	ecdmn0 4264	. . . . . . . . . . . 12 |- (<.A, B>. e. dom R <-> -. [<.A, B>.]R = (/))
26		eceqopreq.2	. . . . . . . . . . . . 13 |- B e. V
27	26	opelxp 3204	. . . . . . . . . . . 12 |- (<.A, B>. e. (S X. S) <-> (A e. S /\ B e. S))
28	23, 25, 27	3bitr3 181	. . . . . . . . . . 11 |- (-. [<.A, B>.]R = (/) <-> (A e. S /\ B e. S))
29	22, 28	syl5ibr 207	. . . . . . . . . 10 |- (-. D e. S -> ((A e. S /\ B e. S) -> -. [<.A, B>.]R = [<.C, D>.]R))
30	29	com12 11	. . . . . . . . 9 |- ((A e. S /\ B e. S) -> (-. D e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
31	30	3adant3 797	. . . . . . . 8 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
32		eleq1 1526	. . . . . . . . . . . 12 |- ((AFD) = (BFC) -> ((AFD) e. S <-> (BFC) e. S))
33		eceqopreq.9	. . . . . . . . . . . . 13 |- ((x e. S /\ y e. S) -> (xFy) e. S)
34	33	caoprcl 4038	. . . . . . . . . . . 12 |- ((B e. S /\ C e. S) -> (BFC) e. S)
35	32, 34	syl5bir 210	. . . . . . . . . . 11 |- ((AFD) = (BFC) -> ((B e. S /\ C e. S) -> (AFD) e. S))
36		eceqopreq.7	. . . . . . . . . . . . 13 |- dom F = (S X. S)
37		eceqopreq.8	. . . . . . . . . . . . 13 |- -. (/) e. S
38	18, 36, 37	ndmoprrcl 4032	. . . . . . . . . . . 12 |- ((AFD) e. S -> (A e. S /\ D e. S))
39	38	pm3.27d 325	. . . . . . . . . . 11 |- ((AFD) e. S -> D e. S)
40	35, 39	syl6com 53	. . . . . . . . . 10 |- ((B e. S /\ C e. S) -> ((AFD) = (BFC) -> D e. S))
41	40	con3d 95	. . . . . . . . 9 |- ((B e. S /\ C e. S) -> (-. D e. S -> -. (AFD) = (BFC)))
42	41	3adant1 795	. . . . . . . 8 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> -. (AFD) = (BFC)))
43	31, 42	jcad 598	. . . . . . 7 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> (-. [<.A, B>.]R = [<.C, D>.]R /\ -. (AFD) = (BFC))))
44		pm5.21 675	. . . . . . 7 |- ((-. [<.A, B>.]R = [<.C, D>.]R /\ -. (AFD) = (BFC)) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))
45	43, 44	syl6 22	. . . . . 6 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))
46	12, 45	pm2.61d 127	. . . . 5 |- ((A e. S /\ B e. S /\ C e. S) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))
47	46	3exp 830	. . . 4 |- (A e. S -> (B e. S -> (C e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))))
48	47	com23 32	. . 3 |- (A e. S -> (C e. S -> (B e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))))
49	48	imp 350	. 2 |- ((A e. S /\ C e. S) -> (B e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))
50	13	biimpcd 155	. . . . . . . . . . 11 |- ([<.A, B>.]R = (/) -> ([<.A, B>.]R = [<.C, D>.]R -> [<.C, D>.]R = (/)))
51	50	con3d 95	. . . . . . . . . 10 |- ([<.A, B>.]R = (/) -> (-. [<.C, D>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
52	28	pm3.27bi 326	. . . . . . . . . 10 |- (-. [<.A, B>.]R = (/) -> B e. S)
53	51, 52	nsyl4 120	. . . . . . . . 9 |- (-. B e. S -> (-. [<.C, D>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
54	53, 20	syl5ibr 207	. . . . . . . 8 |- (-. B e. S -> ((C e. S /\ D e. S) -> -. [<.A, B>.]R = [<.C, D>.]R))
55	54	com12 11	. . . . . . 7 |- ((C e. S /\ D e. S) -> (-. B e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
56	55	3adant1 795	. . . . . 6 |- ((A e. S /\ C e. S /\ D e. S) -> (-. B e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
57	33	caoprcl 4038	. . . . . . . . . 10 |- ((A