Theorem eceqopreq 3249

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

Hypotheses

Ref	Expression
eceqopreq.2	⊢ B ∈ V
eceqopreq.3	⊢ C ∈ V
eceqopreq.4	⊢ D ∈ V
eceqopreq.5	⊢ Er R
eceqopreq.6	⊢ dom R = (S × S)
eceqopreq.7	⊢ dom F = (S × S)
eceqopreq.8	⊢ ¬ ∅ ∈ S
eceqopreq.9	⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S)
eceqopreq.10	⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ (AFD) = (BFC)))

Assertion

Ref	Expression
eceqopreq	⊢ ((A ∈ S ∧ C ∈ 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 ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (A ∈ S ∧ B ∈ S))
2		opelxpi 2455	. . . . . . . . . . 11 ⊢ ((A ∈ S ∧ B ∈ S) → ⟨A, B⟩ ∈ (S × S))
3		eceqopreq.6	. . . . . . . . . . . 12 ⊢ dom R = (S × S)
4	3	eleq2i 1153	. . . . . . . . . . 11 ⊢ (⟨A, B⟩ ∈ dom R ↔ ⟨A, B⟩ ∈ (S × S))
5	2, 4	sylibr 175	. . . . . . . . . 10 ⊢ ((A ∈ S ∧ B ∈ S) → ⟨A, B⟩ ∈ dom R)
6		opex 1893	. . . . . . . . . . 11 ⊢ ⟨C, D⟩ ∈ V
7		eceqopreq.5	. . . . . . . . . . 11 ⊢ Er R
8	6, 7	erthdm 3220	. . . . . . . . . 10 ⊢ (⟨A, B⟩ ∈ dom R → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ ⟨A, B⟩R⟨C, D⟩))
9	1, 5, 8	3syl 21	. . . . . . . . 9 ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ ⟨A, B⟩R⟨C, D⟩))
10		eceqopreq.10	. . . . . . . . 9 ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ (AFD) = (BFC)))
11	9, 10	bitrd 406	. . . . . . . 8 ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
12	11	exp43 301	. . . . . . 7 ⊢ (A ∈ S → (B ∈ S → (C ∈ S → (D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))))
13	12	3imp 608	. . . . . 6 ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → (D ∈ 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⟩ ∈ dom R ↔ ⟨C, D⟩ ∈ (S × S))
18	6	ecdmn0 3217	. . . . . . . . . . . . . 14 ⊢ (⟨C, D⟩ ∈ dom R ↔ ¬ [⟨C, D⟩]R = ∅)
19		eceqopreq.4	. . . . . . . . . . . . . . 15 ⊢ D ∈ V
20	19	opelxp 2452	. . . . . . . . . . . . . 14 ⊢ (⟨C, D⟩ ∈ (S × S) ↔ (C ∈ S ∧ D ∈ S))
21	17, 18, 20	3bitr3 156	. . . . . . . . . . . . 13 ⊢ (¬ [⟨C, D⟩]R = ∅ ↔ (C ∈ S ∧ D ∈ S))
22	21	pm3.27bd 263	. . . . . . . . . . . 12 ⊢ (¬ [⟨C, D⟩]R = ∅ → D ∈ S)
23	16, 22	nsyl4 105	. . . . . . . . . . 11 ⊢ (¬ D ∈ S → (¬ [⟨A, B⟩]R = ∅ → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
24		opex 1893	. . . . . . . . . . . . 13 ⊢ ⟨A, B⟩ ∈ V
25	24	ecdmn0 3217	. . . . . . . . . . . 12 ⊢ (⟨A, B⟩ ∈ dom R ↔ ¬ [⟨A, B⟩]R = ∅)
26		eceqopreq.2	. . . . . . . . . . . . 13 ⊢ B ∈ V
27	26	opelxp 2452	. . . . . . . . . . . 12 ⊢ (⟨A, B⟩ ∈ (S × S) ↔ (A ∈ S ∧ B ∈ S))
28	4, 25, 27	3bitr3 156	. . . . . . . . . . 11 ⊢ (¬ [⟨A, B⟩]R = ∅ ↔ (A ∈ S ∧ B ∈ S))
29	23, 28	syl5ibr 182	. . . . . . . . . 10 ⊢ (¬ D ∈ S → ((A ∈ S ∧ B ∈ S) → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
30	29	com12 13	. . . . . . . . 9 ⊢ ((A ∈ S ∧ B ∈ S) → (¬ D ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
31	30	3adant3 599	. . . . . . . 8 ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → (¬ D ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
32		eleq1 1149	. . . . . . . . . . . . 13 ⊢ ((AFD) = (BFC) → ((AFD) ∈ S ↔ (BFC) ∈ S))
33		eceqopreq.9	. . . . . . . . . . . . . 14 ⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S)
34	33	caoprcl 3066	. . . . . . . . . . . . 13 ⊢ ((B ∈ S ∧ C ∈ S) → (BFC) ∈ S)
35	32, 34	syl5bir 184	. . . . . . . . . . . 12 ⊢ ((AFD) = (BFC) → ((B ∈ S ∧ C ∈ S) → (AFD) ∈ S))
36		eceqopreq.7	. . . . . . . . . . . . . 14 ⊢ dom F = (S × S)
37		eceqopreq.8	. . . . . . . . . . . . . 14 ⊢ ¬ ∅ ∈ S
38	19, 36, 37	ndmoprrcl 3060	. . . . . . . . . . . . 13 ⊢ ((AFD) ∈ S → (A ∈ S ∧ D ∈ S))
39	38	pm3.27d 262	. . . . . . . . . . . 12 ⊢ ((AFD) ∈ S → D ∈ S)
40	35, 39	syl6 23	. . . . . . . . . . 11 ⊢ ((AFD) = (BFC) → ((B ∈ S ∧ C ∈ S) → D ∈ S))
41	40	com12 13	. . . . . . . . . 10 ⊢ ((B ∈ S ∧ C ∈ S) → ((AFD) = (BFC) → D ∈ S))
42	41	con3d 87	. . . . . . . . 9 ⊢ ((B ∈ S ∧ C ∈ S) → (¬ D ∈ S → ¬ (AFD) = (BFC)))
43	42	3adant1 597	. . . . . . . 8 ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → (¬ D ∈ S → ¬ (AFD) = (BFC)))
44	31, 43	jcad 455	. . . . . . 7 ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → (¬ D ∈ 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 ∈ S ∧ B ∈ S ∧ C ∈ S) → (¬ D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
47	13, 46	pm2.61d 112	. . . . 5 ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
48	47	3exp 611	. . . 4 ⊢ (A ∈ S → (B ∈ S → (C ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
49	48	com23 32	. . 3 ⊢ (A ∈ S → (C ∈ S → (B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
50	49	imp 277	. 2 ⊢ ((A ∈ S ∧ C ∈ S) → (B ∈ 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 ∈ S)
54	52, 53	nsyl4 105	. . . . . . . . . 10 ⊢ (¬ B ∈ S → (¬ [⟨C, D⟩]R = ∅ → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
55	54, 21	syl5ibr 182	. . . . . . . . 9 ⊢ (¬ B ∈ S → ((C ∈ S ∧ D ∈ S) → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
56	55	com12 13	. . . . . . . 8 ⊢ ((C ∈ S ∧ D ∈ S) → (¬ B ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
57	56	3adant1 597	. . . . . . 7 ⊢ ((A ∈ S ∧ C ∈ S ∧ D ∈ S) → (¬ B ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
58	33	caoprcl 3066	. . . . . . . . . . . 12 ⊢ ((A ∈ S ∧ D ∈ S) → (AFD) ∈ S)
59	32, 58	syl5bi 183	. . . . . . . . . . 11 ⊢ ((AFD) = (BFC) → ((A ∈ S ∧ D ∈ S) → (BFC) ∈ S))
60		eceqopreq.3	. . . . . . . . . . . . 13 ⊢ C ∈ V
61	60, 36, 37	ndmoprrcl 3060	. . . . . . . . . . . 12 ⊢ ((BFC) ∈ S → (B ∈ S ∧ C ∈ S))
62	61	pm3.26d 258	. . . . . . . . . . 11 ⊢ ((BFC) ∈ S → B ∈ S)
63	59, 62	syl6 23	. . . . . . . . . 10 ⊢ ((AFD) = (BFC) → ((A ∈ S ∧ D ∈ S) → B ∈ S))
64	63	com12 13	. . . . . . . . 9 ⊢ ((A ∈ S ∧ D ∈ S) → ((AFD) = (BFC) → B ∈ S))
65	64	con3d 87	. . . . . . . 8 ⊢ ((A ∈ S ∧ D ∈ S) → (¬ B ∈ S → ¬ (AFD) = (BFC)))
66	65	3adant2 598	. . . . . . 7 ⊢ ((A ∈ S ∧ C ∈ S ∧ D ∈ S) → (¬ B ∈ S → ¬ (AFD) = (BFC)))
67	57, 66	jcad 455	. . . . . 6 ⊢ ((A ∈ S ∧ C ∈ S ∧ D ∈ S) → (¬ B ∈ S → (¬ [⟨A, B⟩]R = [⟨C, D⟩]R ∧ ¬ (AFD) = (BFC))))
68	67, 45	syl6 23	. . . . 5 ⊢ ((A ∈ S ∧ C ∈ S ∧ D ∈ S) → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
69	68	3exp 611	. . . 4 ⊢ (A ∈ S → (C ∈ S → (D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))))
70	69	imp 277	. . 3 ⊢ ((A ∈ S ∧ C ∈ S) → (D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
71		cleq2 1110	. . . . . . . 8 ⊢ ([⟨C, D⟩]R = ∅ → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ [⟨A, B⟩]R = ∅))
72	71, 22	nsyl4 105	. . . . . . 7 ⊢ (¬ D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ [⟨A, B⟩]R = ∅))
73	53	con1i 88	. . . . . . 7 ⊢ (¬ B ∈ S → [⟨A, B⟩]R = ∅)
74	72, 73	syl5bir 184	. . . . . 6 ⊢ (¬ D ∈ S → (¬ B ∈ S → [⟨A, B⟩]R = [⟨C, D⟩]R))
75		pm3.26 256	. . . . . . . . 9 ⊢ ((B ∈ S ∧ C ∈ S) → B ∈ S)
76	75	con3i 90	. . . . . . . 8 ⊢ (¬ B ∈ S → ¬ (B ∈ S ∧ C ∈ S))
77	60, 36	ndmopr 3059	. . . . . . . 8 ⊢ (¬ (B ∈ S ∧ C ∈ S) → (BFC) = ∅)
78		cleq2 1110	. . . . . . . . 9 ⊢ ((BFC) = ∅ → ((AFD) = (BFC) ↔ (AFD) = ∅))
79		pm3.27 260	. . . . . . . . . . 11 ⊢ ((A ∈ S ∧ D ∈ S) → D ∈ S)
80	79	con3i 90	. . . . . . . . . 10 ⊢ (¬ D ∈ S → ¬ (A ∈ S ∧ D ∈ S))
81	19, 36	ndmopr 3059	. . . . . . . . . 10 ⊢ (¬ (A ∈ S ∧ D ∈ S) → (AFD) = ∅)
82	80, 81	syl 12	. . . . . . . . 9 ⊢ (¬ D ∈ S → (AFD) = ∅)
83	78, 82	syl5bir 184	. . . . . . . 8 ⊢ ((BFC) = ∅ → (¬ D ∈ S → (AFD) = (BFC)))
84	76, 77, 83	3syl 21	. . . . . . 7 ⊢ (¬ B ∈ S → (¬ D ∈ S → (AFD) = (BFC)))
85	84	com12 13	. . . . . 6 ⊢ (¬ D ∈ S → (¬ B ∈ S → (AFD) = (BFC)))
86	74, 85	jcad 455	. . . . 5 ⊢ (¬ D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ∧ (AFD) = (BFC))))
87		pm5.1 501	. . . . 5 ⊢ (([⟨A, B⟩]R = [⟨C, D⟩]R ∧ (AFD) = (BFC)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
88	86, 87	syl6 23	. . . 4 ⊢ (¬ D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
89	88	a1i 7	. . 3 ⊢ ((A ∈ S ∧ C ∈ S) → (¬ D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
90	70, 89	pm2.61d 112	. 2 ⊢ ((A ∈ S ∧ C ∈ S) → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
91	50, 90	pm2.61d 112	1 ⊢ ((A ∈ S ∧ C ∈ S) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196   ∧ w3a 581   = wceq 1091   ∈ wcel 1092  Vcvv 1348  ∅c0 1707  ⟨cop 1810   class class class wbr 2054   × cxp 2408  dom cdm 2410  (class class class)co 3001  Er wer 3197  [cec 3198

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438  df-opr 3003  df-er 3200  df-ec 3202

metamath.org