Theorem eceqopreq 3249

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 group(s):   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 256	. . . . . . . . . 10 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (A e. S /\ B e. S))
2		opelxpi 2455	. . . . . . . . . . 11 |- ((A e. S /\ B e. S) -> <.A, B>. e. (S X. S))
3		eceqopreq.6	. . . . . . . . . . . 12 |- dom R = (S X. S)
4	3	eleq2i 1153	. . . . . . . . . . 11 |- (<.A, B>. e. dom R <-> <.A, B>. e. (S X. S))
5	2, 4	sylibr 175	. . . . . . . . . 10 |- ((A e. S /\ B e. S) -> <.A, B>. e. dom R)
6		opex 1893	. . . . . . . . . . 11 |- <.C, D>. e. V
7		eceqopreq.5	. . . . . . . . . . 11 |- Er R
8	6, 7	erthdm 3220	. . . . . . . . . 10 |- (<.A, B>. e. dom R -> ([<.A, B>.]R = [<.C, D>.]R <-> <.A, B>.R<.C, D>.))
9	1, 5, 8	3syl 21	. . . . . . . . 9 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]R = [<.C, D>.]R <-> <.A, B>.R<.C, D>.))
10		eceqopreq.10	. . . . . . . . 9 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (<.A, B>.R<.C, D>. <-> (AFD) = (BFC)))
11	9, 10	bitrd 406	. . . . . . . 8 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))
12	11	exp43 301	. . . . . . 7 |- (A e. S -> (B e. S -> (C e. S -> (D e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))))
13	12	3imp 608	. . . . . 6 |- ((A e. S /\ B e. S /\ C e. S) -> (D e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))
14		cleq1 1107	. . . . . . . . . . . . . 14 |- ([<.A, B>.]R = [<.C, D>.]R -> ([<.A, B>.]R = (/) <-> [<.C, D>.]R = (/)))
15	14	biimprcd 138	. . . . . . . . . . . . 13 |- ([<.C, D>.]R = (/) -> ([<.A, B>.]R = [<.C, D>.]R -> [<.A, B>.]R = (/)))
16	15	con3d 87	. . . . . . . . . . . 12 |- ([<.C, D>.]R = (/) -> (-. [<.A, B>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
17	3	eleq2i 1153	. . . . . . . . . . . . . 14 |- (<.C, D>. e. dom R <-> <.C, D>. e. (S X. S))
18	6	ecdmn0 3217	. . . . . . . . . . . . . 14 |- (<.C, D>. e. dom R <-> -. [<.C, D>.]R = (/))
19		eceqopreq.4	. . . . . . . . . . . . . . 15 |- D e. V
20	19	opelxp 2452	. . . . . . . . . . . . . 14 |- (<.C, D>. e. (S X. S) <-> (C e. S /\ D e. S))
21	17, 18, 20	3bitr3 156	. . . . . . . . . . . . 13 |- (-. [<.C, D>.]R = (/) <-> (C e. S /\ D e. S))
22	21	pm3.27bd 263	. . . . . . . . . . . 12 |- (-. [<.C, D>.]R = (/) -> D e. S)
23	16, 22	nsyl4 105	. . . . . . . . . . 11 |- (-. D e. S -> (-. [<.A, B>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
24		opex 1893	. . . . . . . . . . . . 13 |- <.A, B>. e. V
25	24	ecdmn0 3217	. . . . . . . . . . . 12 |- (<.A, B>. e. dom R <-> -. [<.A, B>.]R = (/))
26		eceqopreq.2	. . . . . . . . . . . . 13 |- B e. V
27	26	opelxp 2452	. . . . . . . . . . . 12 |- (<.A, B>. e. (S X. S) <-> (A e. S /\ B e. S))
28	4, 25, 27	3bitr3 156	. . . . . . . . . . 11 |- (-. [<.A, B>.]R = (/) <-> (A e. S /\ B e. S))
29	23, 28	syl5ibr 182	. . . . . . . . . 10 |- (-. D e. S -> ((A e. S /\ B e. S) -> -. [<.A, B>.]R = [<.C, D>.]R))
30	29	com12 13	. . . . . . . . 9 |- ((A e. S /\ B e. S) -> (-. D e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
31	30	3adant3 599	. . . . . . . 8 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
32		eleq1 1149	. . . . . . . . . . . . 13 |- ((AFD) = (BFC) -> ((AFD) e. S <-> (BFC) e. S))
33		eceqopreq.9	. . . . . . . . . . . . . 14 |- ((x e. S /\ y e. S) -> (xFy) e. S)
34	33	caoprcl 3066	. . . . . . . . . . . . 13 |- ((B e. S /\ C e. S) -> (BFC) e. S)
35	32, 34	syl5bir 184	. . . . . . . . . . . 12 |- ((AFD) = (BFC) -> ((B e. S /\ C e. S) -> (AFD) e. S))
36		eceqopreq.7	. . . . . . . . . . . . . 14 |- dom F = (S X. S)
37		eceqopreq.8	. . . . . . . . . . . . . 14 |- -. (/) e. S
38	19, 36, 37	ndmoprrcl 3060	. . . . . . . . . . . . 13 |- ((AFD) e. S -> (A e. S /\ D e. S))
39	38	pm3.27d 262	. . . . . . . . . . . 12 |- ((AFD) e. S -> D e. S)
40	35, 39	syl6 23	. . . . . . . . . . 11 |- ((AFD) = (BFC) -> ((B e. S /\ C e. S) -> D e. S))
41	40	com12 13	. . . . . . . . . 10 |- ((B e. S /\ C e. S) -> ((AFD) = (BFC) -> D e. S))
42	41	con3d 87	. . . . . . . . 9 |- ((B e. S /\ C e. S) -> (-. D e. S -> -. (AFD) = (BFC)))
43	42	3adant1 597	. . . . . . . 8 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> -. (AFD) = (BFC)))
44	31, 43	jcad 455	. . . . . . 7 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> (-. [<.A, B>.]R = [<.C, D>.]R /\ -. (AFD) = (BFC))))
45		pm5.21 502	. . . . . . 7 |- ((-. [<.A, B>.]R = [<.C, D>.]R /\ -. (AFD) = (BFC)) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))
46	44, 45	syl6 23	. . . . . 6 |- ((A e. S /\ B e. S /\ C e. S) -> (-. D e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))
47	13, 46	pm2.61d 112	. . . . 5 |- ((A e. S /\ B e. S /\ C e. S) -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))
48	47	3exp 611	. . . 4 |- (A e. S -> (B e. S -> (C e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))))
49	48	com23 32	. . 3 |- (A e. S -> (C e. S -> (B e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC)))))
50	49	imp 277	. 2 |- ((A e. S /\ C e. S) -> (B e. S -> ([<.A, B>.]R = [<.C, D>.]R <-> (AFD) = (BFC))))
51	14	biimpcd 137	. . . . . . . . . . . 12 |- ([<.A, B>.]R = (/) -> ([<.A, B>.]R = [<.C, D>.]R -> [<.C, D>.]R = (/)))
52	51	con3d 87	. . . . . . . . . . 11 |- ([<.A, B>.]R = (/) -> (-. [<.C, D>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
53	28	pm3.27bd 263	. . . . . . . . . . 11 |- (-. [<.A, B>.]R = (/) -> B e. S)
54	52, 53	nsyl4 105	. . . . . . . . . 10 |- (-. B e. S -> (-. [<.C, D>.]R = (/) -> -. [<.A, B>.]R = [<.C, D>.]R))
55	54, 21	syl5ibr 182	. . . . . . . . 9 |- (-. B e. S -> ((C e. S /\ D e. S) -> -. [<.A, B>.]R = [<.C, D>.]R))
56	55	com12 13	. . . . . . . 8 |- ((C e. S /\ D e. S) -> (-. B e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
57	56	3adant1 597	. . . . . . 7 |- ((A e. S /\ C e. S /\ D e. S) -> (-. B e. S -> -. [<.A, B>.]R = [<.C, D>.]R))
58	33	caoprcl 3066	. . . . . . . . . . . 12 |- ((A e. S /\ D e. S) -> (AFD) e. S)
59	32, 58	syl5bi&nb