Theorem eceqopreq 4319

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 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 ∈ S ⋀ B ∈ S) ⋀ (C ∈ S ⋀ D ∈ S)) → (A ∈ S ⋀ B ∈ S))
2		opelxpi 3223	. . . . . . . . . . 11 ⊢ ((A ∈ S ⋀ B ∈ S) → ⟨A, B⟩ ∈ (S × S))
3		eceqopreq.6	. . . . . . . . . . 11 ⊢ dom R = (S × S)
4	2, 3	syl6eleqr 1562	. . . . . . . . . 10 ⊢ ((A ∈ S ⋀ B ∈ S) → ⟨A, B⟩ ∈ dom R)
5		opex 2788	. . . . . . . . . . 11 ⊢ ⟨C, D⟩ ∈ V
6		eceqopreq.5	. . . . . . . . . . 11 ⊢ Er R
7	5, 6	erthdm 4289	. . . . . . . . . 10 ⊢ (⟨A, B⟩ ∈ dom R → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ ⟨A, B⟩R⟨C, D⟩))
8	1, 4, 7	3syl 20	. . . . . . . . 9 ⊢ (((A ∈ S ⋀ B ∈ S) ⋀ (C ∈ S ⋀ D ∈ S)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ ⟨A, B⟩R⟨C, D⟩))
9		eceqopreq.10	. . . . . . . . 9 ⊢ (((A ∈ S ⋀ B ∈ S) ⋀ (C ∈ S ⋀ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ (AFD) = (BFC)))
10	8, 9	bitrd 530	. . . . . . . 8 ⊢ (((A ∈ S ⋀ B ∈ S) ⋀ (C ∈ S ⋀ D ∈ S)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
11	10	exp43 386	. . . . . . 7 ⊢ (A ∈ S → (B ∈ S → (C ∈ S → (D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))))
12	11	3imp 829	. . . . . 6 ⊢ ((A ∈ S ⋀ B ∈ S ⋀ C ∈ S) → (D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
13		eqeq1 1484	. . . . . . . . . . . . . 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 1541	. . . . . . . . . . . . . 14 ⊢ (⟨C, D⟩ ∈ dom R ↔ ⟨C, D⟩ ∈ (S × S))
17	5	ecdmn0 4286	. . . . . . . . . . . . . 14 ⊢ (⟨C, D⟩ ∈ dom R ↔ ¬ [⟨C, D⟩]R = ∅)
18		eceqopreq.4	. . . . . . . . . . . . . . 15 ⊢ D ∈ V
19	18	opelxp 3220	. . . . . . . . . . . . . 14 ⊢ (⟨C, D⟩ ∈ (S × S) ↔ (C ∈ S ⋀ D ∈ S))
20	16, 17, 19	3bitr3 181	. . . . . . . . . . . . 13 ⊢ (¬ [⟨C, D⟩]R = ∅ ↔ (C ∈ S ⋀ D ∈ S))
21	20	pm3.27bi 326	. . . . . . . . . . . 12 ⊢ (¬ [⟨C, D⟩]R = ∅ → D ∈ S)
22	15, 21	nsyl4 120	. . . . . . . . . . 11 ⊢ (¬ D ∈ S → (¬ [⟨A, B⟩]R = ∅ → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
23	3	eleq2i 1541	. . . . . . . . . . . 12 ⊢ (⟨A, B⟩ ∈ dom R ↔ ⟨A, B⟩ ∈ (S × S))
24		opex 2788	. . . . . . . . . . . . 13 ⊢ ⟨A, B⟩ ∈ V
25	24	ecdmn0 4286	. . . . . . . . . . . 12 ⊢ (⟨A, B⟩ ∈ dom R ↔ ¬ [⟨A, B⟩]R = ∅)
26		eceqopreq.2	. . . . . . . . . . . . 13 ⊢ B ∈ V
27	26	opelxp 3220	. . . . . . . . . . . 12 ⊢ (⟨A, B⟩ ∈ (S × S) ↔ (A ∈ S ⋀ B ∈ S))
28	23, 25, 27	3bitr3 181	. . . . . . . . . . 11 ⊢ (¬ [⟨A, B⟩]R = ∅ ↔ (A ∈ S ⋀ B ∈ S))
29	22, 28	syl5ibr 207	. . . . . . . . . 10 ⊢ (¬ D ∈ S → ((A ∈ S ⋀ B ∈ S) → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
30	29	com12 11	. . . . . . . . 9 ⊢ ((A ∈ S ⋀ B ∈ S) → (¬ D ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
31	30	3adant3 801	. . . . . . . 8 ⊢ ((A ∈ S ⋀ B ∈ S ⋀ C ∈ S) → (¬ D ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
32		eleq1 1537	. . . . . . . . . . . 12 ⊢ ((AFD) = (BFC) → ((AFD) ∈ S ↔ (BFC) ∈ S))
33		eceqopreq.9	. . . . . . . . . . . . 13 ⊢ ((x ∈ S ⋀ y ∈ S) → (xFy) ∈ S)
34	33	caoprcl 4058	. . . . . . . . . . . 12 ⊢ ((B ∈ S ⋀ C ∈ S) → (BFC) ∈ S)
35	32, 34	syl5bir 210	. . . . . . . . . . 11 ⊢ ((AFD) = (BFC) → ((B ∈ S ⋀ C ∈ S) → (AFD) ∈ S))
36		eceqopreq.7	. . . . . . . . . . . . 13 ⊢ dom F = (S × S)
37		eceqopreq.8	. . . . . . . . . . . . 13 ⊢ ¬ ∅ ∈ S
38	18, 36, 37	ndmoprrcl 4052	. . . . . . . . . . . 12 ⊢ ((AFD) ∈ S → (A ∈ S ⋀ D ∈ S))
39	38	pm3.27d 325	. . . . . . . . . . 11 ⊢ ((AFD) ∈ S → D ∈ S)
40	35, 39	syl6com 53	. . . . . . . . . 10 ⊢ ((B ∈ S ⋀ C ∈ S) → ((AFD) = (BFC) → D ∈ S))
41	40	con3d 95	. . . . . . . . 9 ⊢ ((B ∈ S ⋀ C ∈ S) → (¬ D ∈ S → ¬ (AFD) = (BFC)))
42	41	3adant1 799	. . . . . . . 8 ⊢ ((A ∈ S ⋀ B ∈ S ⋀ C ∈ S) → (¬ D ∈ S → ¬ (AFD) = (BFC)))
43	31, 42	jcad 602	. . . . . . 7 ⊢ ((A ∈ S ⋀ B ∈ S ⋀ C ∈ S) → (¬ D ∈ S → (¬ [⟨A, B⟩]R = [⟨C, D⟩]R ⋀ ¬ (AFD) = (BFC))))
44		pm5.21 679	. . . . . . 7 ⊢ ((¬ [⟨A, B⟩]R = [⟨C, D⟩]R ⋀ ¬ (AFD) = (BFC)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
45	43, 44	syl6 22	. . . . . 6 ⊢ ((A ∈ S ⋀ B ∈ S ⋀ C ∈ S) → (¬ D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
46	12, 45	pm2.61d 127	. . . . 5 ⊢ ((A ∈ S ⋀ B ∈ S ⋀ C ∈ S) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
47	46	3exp 834	. . . 4 ⊢ (A ∈ S → (B ∈ S → (C ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
48	47	com23 32	. . 3 ⊢ (A ∈ S → (C ∈ S → (B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
49	48	imp 350	. 2 ⊢ ((A ∈ S ⋀ C ∈ S) → (B ∈ 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 ∈ S)
53	51, 52	nsyl4 120	. . . . . . . . 9 ⊢ (¬ B ∈ S → (¬ [⟨C, D⟩]R = ∅ → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
54	53, 20	syl5ibr 207	. . . . . . . 8 ⊢ (¬ B ∈ S → ((C ∈ S ⋀ D ∈ S) → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
55	54	com12 11	. . . . . . 7 ⊢ ((C ∈ S ⋀ D ∈ S) → (¬ B ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
56	55	3adant1 799	. . . . . 6 ⊢ ((A ∈ S ⋀ C ∈ S ⋀ D ∈ S) → (¬ B ∈ S → ¬ [⟨A, B⟩]R = [⟨C, D⟩]R))
57	33	caoprcl 4058	. . . . . . . . . 10 ⊢ ((A ∈ S ⋀ D ∈ S) → (AFD) ∈ S)
58	32, 57	syl5bi 208	. . . . . . . . 9 ⊢ ((AFD) = (BFC) → ((A ∈ S ⋀ D ∈ S) → (BFC) ∈ S))
59		eceqopreq.3	. . . . . . . . . . 11 ⊢ C ∈ V
60	59, 36, 37	ndmoprrcl 4052	. . . . . . . . . 10 ⊢ ((BFC) ∈ S → (B ∈ S ⋀ C ∈ S))
61	60	pm3.26d 321	. . . . . . . . 9 ⊢ ((BFC) ∈ S → B ∈ S)
62	58, 61	syl6com 53	. . . . . . . 8 ⊢ ((A ∈ S ⋀ D ∈ S) → ((AFD) = (BFC) → B ∈ S))
63	62	con3d 95	. . . . . . 7 ⊢ ((A ∈ S ⋀ D ∈ S) → (¬ B ∈ S → ¬ (AFD) = (BFC)))
64	63	3adant2 800	. . . . . 6 ⊢ ((A ∈ S ⋀ C ∈ S ⋀ D ∈ S) → (¬ B ∈ S → ¬ (AFD) = (BFC)))
65	56, 64	jcad 602	. . . . 5 ⊢ ((A ∈ S ⋀ C ∈ S ⋀ D ∈ S) → (¬ B ∈ S → (¬ [⟨A, B⟩]R = [⟨C, D⟩]R ⋀ ¬ (AFD) = (BFC))))
66	65, 44	syl6 22	. . . 4 ⊢ ((A ∈ S ⋀ C ∈ S ⋀ D ∈ S) → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
67	66	3expia 837	. . 3 ⊢ ((A ∈ S ⋀ C ∈ S) → (D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))))
68		eqeq2 1487	. . . . . . 7 ⊢ ([⟨C, D⟩]R = ∅ → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ [⟨A, B⟩]R = ∅))
69	68, 21	nsyl4 120	. . . . . 6 ⊢ (¬ D ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ [⟨A, B⟩]R = ∅))
70	52	con1i 96	. . . . . 6 ⊢ (¬ B ∈ S → [⟨A, B⟩]R = ∅)
71	69, 70	syl5bir 210	. . . . 5 ⊢ (¬ D ∈ S → (¬ B ∈ S → [⟨A, B⟩]R = [⟨C, D⟩]R))
72		pm3.26 319	. . . . . . . 8 ⊢ ((B ∈ S ⋀ C ∈ S) → B ∈ S)
73	72	con3i 98	. . . . . . 7 ⊢ (¬ B ∈ S → ¬ (B ∈ S ⋀ C ∈ S))
74	59, 36	ndmopr 4051	. . . . . . 7 ⊢ (¬ (B ∈ S ⋀ C ∈ S) → (BFC) = ∅)
75		eqeq2 1487	. . . . . . . 8 ⊢ ((BFC) = ∅ → ((AFD) = (BFC) ↔ (AFD) = ∅))
76		pm3.27 323	. . . . . . . . . 10 ⊢ ((A ∈ S ⋀ D ∈ S) → D ∈ S)
77	76	con3i 98	. . . . . . . . 9 ⊢ (¬ D ∈ S → ¬ (A ∈ S ⋀ D ∈ S))
78	18, 36	ndmopr 4051	. . . . . . . . 9 ⊢ (¬ (A ∈ S ⋀ D ∈ S) → (AFD) = ∅)
79	77, 78	syl 10	. . . . . . . 8 ⊢ (¬ D ∈ S → (AFD) = ∅)
80	75, 79	syl5bir 210	. . . . . . 7 ⊢ ((BFC) = ∅ → (¬ D ∈ S → (AFD) = (BFC)))
81	73, 74, 80	3syl 20	. . . . . 6 ⊢ (¬ B ∈ S → (¬ D ∈ S → (AFD) = (BFC)))
82	81	com12 11	. . . . 5 ⊢ (¬ D ∈ S → (¬ B ∈ S → (AFD) = (BFC)))
83	71, 82	jcad 602	. . . 4 ⊢ (¬ D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ⋀ (AFD) = (BFC))))
84		pm5.1 678	. . . 4 ⊢ (([⟨A, B⟩]R = [⟨C, D⟩]R ⋀ (AFD) = (BFC)) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))
85	83, 84	syl6 22	. . 3 ⊢ (¬ D ∈ S → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
86	67, 85	pm2.61d1 128	. 2 ⊢ ((A ∈ S ⋀ C ∈ S) → (¬ B ∈ S → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))))
87	49, 86	pm2.61d 127	1 ⊢ ((A ∈ S ⋀ C ∈ S) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 777   = wceq 958   ∈ wcel 960  Vcvv 1814  ∅c0 2283  ⟨cop 2415   class class class wbr 2624   × cxp 3174  dom cdm 3176  (class class class)co 3969  Er wer 4264  [cec 4265

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204  df-opr 3971  df-er 4267  df-ec 4269

Copyright terms: Public domain