Metamath Proof Explorer

Theorem propeqop

Description: Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020) (Proof shortened by AV, 16-Jun-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a ⊢ 𝐴 ∈ V
snopeqop.b ⊢ 𝐵 ∈ V
propeqop.c ⊢ 𝐶 ∈ V
propeqop.d ⊢ 𝐷 ∈ V
propeqop.e ⊢ 𝐸 ∈ V
propeqop.f ⊢ 𝐹 ∈ V
Assertion propeqop ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )

Proof

Step Hyp Ref Expression
1 snopeqop.a ⊢ 𝐴 ∈ V
2 snopeqop.b ⊢ 𝐵 ∈ V
3 propeqop.c ⊢ 𝐶 ∈ V
4 propeqop.d ⊢ 𝐷 ∈ V
5 propeqop.e ⊢ 𝐸 ∈ V
6 propeqop.f ⊢ 𝐹 ∈ V
7 1 2 opeqsn ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 } ↔ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) )
8 3 4 5 6 opeqpr ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ↔ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) )
9 7 8 anbi12i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ) ↔ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) )
10 1 2 5 6 opeqpr ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 , 𝐹 } ↔ ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) )
11 3 4 opeqsn ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ↔ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) )
12 10 11 anbi12i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 , 𝐹 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ) ↔ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) )
13 9 12 orbi12i ⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ) ∨ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 , 𝐹 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ) ) ↔ ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) )
14 eqcom ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ ↔ ⟨ 𝐸 , 𝐹 ⟩ = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
15 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
16 opex ⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
17 5 6 15 16 opeqpr ⊢ ( ⟨ 𝐸 , 𝐹 ⟩ = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ) ∨ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 , 𝐹 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ) ) )
18 14 17 bitri ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ) ∨ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐸 , 𝐹 } ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ) ) )
19 simpl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) → 𝐴 = 𝐵 )
20 simpr ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐸 = { 𝐴 } )
21 19 20 anim12i ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) )
22 sneq ⊢ ( 𝐴 = 𝐶 → { 𝐴 } = { 𝐶 } )
23 22 eqeq2d ⊢ ( 𝐴 = 𝐶 → ( 𝐸 = { 𝐴 } ↔ 𝐸 = { 𝐶 } ) )
24 23 biimpa ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐸 = { 𝐶 } )
25 24 adantl ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → 𝐸 = { 𝐶 } )
26 preq1 ⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝐷 } = { 𝐶 , 𝐷 } )
27 26 adantr ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → { 𝐴 , 𝐷 } = { 𝐶 , 𝐷 } )
28 27 eqeq2d ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → ( 𝐹 = { 𝐴 , 𝐷 } ↔ 𝐹 = { 𝐶 , 𝐷 } ) )
29 28 biimpcd ⊢ ( 𝐹 = { 𝐴 , 𝐷 } → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐹 = { 𝐶 , 𝐷 } ) )
30 29 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐹 = { 𝐶 , 𝐷 } ) )
31 30 imp ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → 𝐹 = { 𝐶 , 𝐷 } )
32 25 31 jca ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) )
33 32 orcd ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) )
34 21 33 jca ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) )
35 34 orcd ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) )
36 35 ex ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) ) )
37 simpr ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) → 𝐹 = { 𝐴 , 𝐵 } )
38 20 37 anim12i ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) → ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) )
39 38 ancoms ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) )
40 39 orcd ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) )
41 simpl ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐴 = 𝐶 )
42 41 eqeq1d ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → ( 𝐴 = 𝐷 ↔ 𝐶 = 𝐷 ) )
43 42 biimpcd ⊢ ( 𝐴 = 𝐷 → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐶 = 𝐷 ) )
44 43 adantr ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → 𝐶 = 𝐷 ) )
45 44 imp ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → 𝐶 = 𝐷 )
46 23 biimpd ⊢ ( 𝐴 = 𝐶 → ( 𝐸 = { 𝐴 } → 𝐸 = { 𝐶 } ) )
47 46 a1dd ⊢ ( 𝐴 = 𝐶 → ( 𝐸 = { 𝐴 } → ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) → 𝐸 = { 𝐶 } ) ) )
48 47 imp ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) → 𝐸 = { 𝐶 } ) )
49 48 impcom ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → 𝐸 = { 𝐶 } )
50 45 49 jca ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) )
51 40 50 jca ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) )
52 51 olcd ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) )
53 52 ex ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) ) )
54 36 53 jaoi ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) ) )
55 54 impcom ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) )
56 eqeq1 ⊢ ( 𝐸 = { 𝐶 } → ( 𝐸 = { 𝐴 } ↔ { 𝐶 } = { 𝐴 } ) )
57 3 sneqr ⊢ ( { 𝐶 } = { 𝐴 } → 𝐶 = 𝐴 )
58 57 eqcomd ⊢ ( { 𝐶 } = { 𝐴 } → 𝐴 = 𝐶 )
59 56 58 biimtrdi ⊢ ( 𝐸 = { 𝐶 } → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐶 ) )
60 59 adantr ⊢ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐶 ) )
61 eqeq1 ⊢ ( 𝐸 = { 𝐶 , 𝐷 } → ( 𝐸 = { 𝐴 } ↔ { 𝐶 , 𝐷 } = { 𝐴 } ) )
62 3 4 preqsn ⊢ ( { 𝐶 , 𝐷 } = { 𝐴 } ↔ ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) )
63 eqtr ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) → 𝐶 = 𝐴 )
64 63 eqcomd ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) → 𝐴 = 𝐶 )
65 62 64 sylbi ⊢ ( { 𝐶 , 𝐷 } = { 𝐴 } → 𝐴 = 𝐶 )
66 61 65 biimtrdi ⊢ ( 𝐸 = { 𝐶 , 𝐷 } → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐶 ) )
67 66 adantr ⊢ ( ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐶 ) )
68 60 67 jaoi ⊢ ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐶 ) )
69 68 com12 ⊢ ( 𝐸 = { 𝐴 } → ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) → 𝐴 = 𝐶 ) )
70 69 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) → 𝐴 = 𝐶 ) )
71 70 impcom ⊢ ( ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → 𝐴 = 𝐶 )
72 simpr ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → 𝐸 = { 𝐴 } )
73 72 adantl ⊢ ( ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → 𝐸 = { 𝐴 } )
74 71 73 jca ⊢ ( ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) )
75 simpl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → 𝐴 = 𝐵 )
76 75 adantr ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ) → 𝐴 = 𝐵 )
77 eqeq1 ⊢ ( 𝐸 = { 𝐴 } → ( 𝐸 = { 𝐶 } ↔ { 𝐴 } = { 𝐶 } ) )
78 1 sneqr ⊢ ( { 𝐴 } = { 𝐶 } → 𝐴 = 𝐶 )
79 78 eqcomd ⊢ ( { 𝐴 } = { 𝐶 } → 𝐶 = 𝐴 )
80 77 79 biimtrdi ⊢ ( 𝐸 = { 𝐴 } → ( 𝐸 = { 𝐶 } → 𝐶 = 𝐴 ) )
81 80 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → ( 𝐸 = { 𝐶 } → 𝐶 = 𝐴 ) )
82 81 impcom ⊢ ( ( 𝐸 = { 𝐶 } ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → 𝐶 = 𝐴 )
83 82 preq1d ⊢ ( ( 𝐸 = { 𝐶 } ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → { 𝐶 , 𝐷 } = { 𝐴 , 𝐷 } )
84 83 eqeq2d ⊢ ( ( 𝐸 = { 𝐶 } ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐹 = { 𝐶 , 𝐷 } ↔ 𝐹 = { 𝐴 , 𝐷 } ) )
85 84 biimpd ⊢ ( ( 𝐸 = { 𝐶 } ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → ( 𝐹 = { 𝐶 , 𝐷 } → 𝐹 = { 𝐴 , 𝐷 } ) )
86 85 impancom ⊢ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) → ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → 𝐹 = { 𝐴 , 𝐷 } ) )
87 86 impcom ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ) → 𝐹 = { 𝐴 , 𝐷 } )
88 76 87 jca ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ) → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) )
89 88 ex ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) )
90 eqcom ⊢ ( 𝐷 = 𝐴 ↔ 𝐴 = 𝐷 )
91 90 bilani ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) → 𝐴 = 𝐷 )
92 91 adantr ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐷 )
93 92 adantr ⊢ ( ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) ∧ 𝐹 = { 𝐶 } ) → 𝐴 = 𝐷 )
94 simpr ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
95 64 eqeq1d ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) → ( 𝐴 = 𝐵 ↔ 𝐶 = 𝐵 ) )
96 95 biimpa ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → 𝐶 = 𝐵 )
97 96 eqcomd ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → 𝐵 = 𝐶 )
98 1 2 preqsn ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) )
99 94 97 98 sylanbrc ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐶 } )
100 99 eqcomd ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → { 𝐶 } = { 𝐴 , 𝐵 } )
101 100 eqeq2d ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → ( 𝐹 = { 𝐶 } ↔ 𝐹 = { 𝐴 , 𝐵 } ) )
102 101 biimpa ⊢ ( ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) ∧ 𝐹 = { 𝐶 } ) → 𝐹 = { 𝐴 , 𝐵 } )
103 93 102 jca ⊢ ( ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) ∧ 𝐹 = { 𝐶 } ) → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) )
104 103 ex ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) ∧ 𝐴 = 𝐵 ) → ( 𝐹 = { 𝐶 } → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) )
105 104 ex ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) → ( 𝐴 = 𝐵 → ( 𝐹 = { 𝐶 } → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
106 105 com23 ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐷 = 𝐴 ) → ( 𝐹 = { 𝐶 } → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
107 62 106 sylbi ⊢ ( { 𝐶 , 𝐷 } = { 𝐴 } → ( 𝐹 = { 𝐶 } → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
108 61 107 biimtrdi ⊢ ( 𝐸 = { 𝐶 , 𝐷 } → ( 𝐸 = { 𝐴 } → ( 𝐹 = { 𝐶 } → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) ) )
109 108 com23 ⊢ ( 𝐸 = { 𝐶 , 𝐷 } → ( 𝐹 = { 𝐶 } → ( 𝐸 = { 𝐴 } → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) ) )
110 109 imp ⊢ ( ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) → ( 𝐸 = { 𝐴 } → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
111 110 com13 ⊢ ( 𝐴 = 𝐵 → ( 𝐸 = { 𝐴 } → ( ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
112 111 imp ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → ( ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) )
113 89 112 orim12d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) → ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
114 113 impcom ⊢ ( ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) )
115 74 114 jca ⊢ ( ( ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ∧ ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
116 115 ancoms ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
117 eqeq1 ⊢ ( 𝐸 = { 𝐶 } → ( 𝐸 = { 𝐴 , 𝐵 } ↔ { 𝐶 } = { 𝐴 , 𝐵 } ) )
118 eqcom ⊢ ( { 𝐶 } = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐶 } )
119 118 98 bitri ⊢ ( { 𝐶 } = { 𝐴 , 𝐵 } ↔ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) )
120 eqtr ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐶 )
121 120 adantr ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐸 = { 𝐶 } ) → 𝐴 = 𝐶 )
122 120 eqcomd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐶 = 𝐴 )
123 sneq ⊢ ( 𝐶 = 𝐴 → { 𝐶 } = { 𝐴 } )
124 122 123 syl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → { 𝐶 } = { 𝐴 } )
125 124 eqeq2d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐸 = { 𝐶 } ↔ 𝐸 = { 𝐴 } ) )
126 125 biimpa ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐸 = { 𝐶 } ) → 𝐸 = { 𝐴 } )
127 121 126 jca ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐸 = { 𝐶 } ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) )
128 127 ex ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐸 = { 𝐶 } → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) )
129 128 a1i13 ⊢ ( 𝐶 = 𝐷 → ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐹 = { 𝐴 } → ( 𝐸 = { 𝐶 } → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) ) )
130 129 com14 ⊢ ( 𝐸 = { 𝐶 } → ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐹 = { 𝐴 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) ) )
131 119 130 biimtrid ⊢ ( 𝐸 = { 𝐶 } → ( { 𝐶 } = { 𝐴 , 𝐵 } → ( 𝐹 = { 𝐴 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) ) )
132 117 131 sylbid ⊢ ( 𝐸 = { 𝐶 } → ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐹 = { 𝐴 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) ) )
133 132 com24 ⊢ ( 𝐸 = { 𝐶 } → ( 𝐶 = 𝐷 → ( 𝐹 = { 𝐴 } → ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) ) )
134 133 impcom ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐹 = { 𝐴 } → ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) )
135 134 com13 ⊢ ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐹 = { 𝐴 } → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) ) )
136 135 imp ⊢ ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) )
137 59 adantl ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐶 ) )
138 137 com12 ⊢ ( 𝐸 = { 𝐴 } → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → 𝐴 = 𝐶 ) )
139 138 adantr ⊢ ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → 𝐴 = 𝐶 ) )
140 139 imp ⊢ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) → 𝐴 = 𝐶 )
141 simpl ⊢ ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) → 𝐸 = { 𝐴 } )
142 141 adantr ⊢ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) → 𝐸 = { 𝐴 } )
143 140 142 jca ⊢ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) )
144 143 ex ⊢ ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) )
145 136 144 jaoi ⊢ ( ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ) )
146 145 impcom ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ∧ ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) )
147 eqeq1 ⊢ ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐸 = { 𝐶 } ↔ { 𝐴 , 𝐵 } = { 𝐶 } ) )
148 simpl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )
149 148 adantr ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) → 𝐴 = 𝐵 )
150 149 adantr ⊢ ( ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) ∧ 𝐹 = { 𝐴 } ) → 𝐴 = 𝐵 )
151 eqtr ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐶 = 𝐷 ) → 𝐴 = 𝐷 )
152 dfsn2 ⊢ { 𝐴 } = { 𝐴 , 𝐴 }
153 preq2 ⊢ ( 𝐴 = 𝐷 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐷 } )
154 152 153 eqtrid ⊢ ( 𝐴 = 𝐷 → { 𝐴 } = { 𝐴 , 𝐷 } )
155 151 154 syl ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐶 = 𝐷 ) → { 𝐴 } = { 𝐴 , 𝐷 } )
156 155 ex ⊢ ( 𝐴 = 𝐶 → ( 𝐶 = 𝐷 → { 𝐴 } = { 𝐴 , 𝐷 } ) )
157 120 156 syl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐶 = 𝐷 → { 𝐴 } = { 𝐴 , 𝐷 } ) )
158 157 imp ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) → { 𝐴 } = { 𝐴 , 𝐷 } )
159 158 eqeq2d ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) → ( 𝐹 = { 𝐴 } ↔ 𝐹 = { 𝐴 , 𝐷 } ) )
160 159 biimpa ⊢ ( ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) ∧ 𝐹 = { 𝐴 } ) → 𝐹 = { 𝐴 , 𝐷 } )
161 150 160 jca ⊢ ( ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) ∧ 𝐹 = { 𝐴 } ) → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) )
162 161 ex ⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∧ 𝐶 = 𝐷 ) → ( 𝐹 = { 𝐴 } → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) )
163 162 ex ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐶 = 𝐷 → ( 𝐹 = { 𝐴 } → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) )
164 163 com23 ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐹 = { 𝐴 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) )
165 98 164 sylbi ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 } → ( 𝐹 = { 𝐴 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) )
166 147 165 biimtrdi ⊢ ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐸 = { 𝐶 } → ( 𝐹 = { 𝐴 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) ) )
167 166 com23 ⊢ ( 𝐸 = { 𝐴 , 𝐵 } → ( 𝐹 = { 𝐴 } → ( 𝐸 = { 𝐶 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) ) )
168 167 imp ⊢ ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) → ( 𝐸 = { 𝐶 } → ( 𝐶 = 𝐷 → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) )
169 168 com13 ⊢ ( 𝐶 = 𝐷 → ( 𝐸 = { 𝐶 } → ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) ) )
170 169 imp ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) → ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ) )
171 80 imp ⊢ ( ( 𝐸 = { 𝐴 } ∧ 𝐸 = { 𝐶 } ) → 𝐶 = 𝐴 )
172 171 eqeq1d ⊢ ( ( 𝐸 = { 𝐴 } ∧ 𝐸 = { 𝐶 } ) → ( 𝐶 = 𝐷 ↔ 𝐴 = 𝐷 ) )
173 172 biimpd ⊢ ( ( 𝐸 = { 𝐴 } ∧ 𝐸 = { 𝐶 } ) → ( 𝐶 = 𝐷 → 𝐴 = 𝐷 ) )
174 173 ex ⊢ ( 𝐸 = { 𝐴 } → ( 𝐸 = { 𝐶 } → ( 𝐶 = 𝐷 → 𝐴 = 𝐷 ) ) )
175 174 com13 ⊢ ( 𝐶 = 𝐷 → ( 𝐸 = { 𝐶 } → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐷 ) ) )
176 175 imp ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( 𝐸 = { 𝐴 } → 𝐴 = 𝐷 ) )
177 176 anim1d ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) → ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) )
178 170 177 orim12d ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) → ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
179 178 imp ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ∧ ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) → ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) )
180 146 179 jca ⊢ ( ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ∧ ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
181 180 ex ⊢ ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) ) )
182 181 com12 ⊢ ( ( ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ∨ ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) ) )
183 182 orcoms ⊢ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) → ( ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) ) )
184 183 imp ⊢ ( ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
185 116 184 jaoi ⊢ ( ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
186 55 185 impbii ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) ↔ ( ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐸 = { 𝐶 } ∧ 𝐹 = { 𝐶 , 𝐷 } ) ∨ ( 𝐸 = { 𝐶 , 𝐷 } ∧ 𝐹 = { 𝐶 } ) ) ) ∨ ( ( ( 𝐸 = { 𝐴 } ∧ 𝐹 = { 𝐴 , 𝐵 } ) ∨ ( 𝐸 = { 𝐴 , 𝐵 } ∧ 𝐹 = { 𝐴 } ) ) ∧ ( 𝐶 = 𝐷 ∧ 𝐸 = { 𝐶 } ) ) ) )
187 13 18 186 3bitr4i ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )