Metamath Proof Explorer

Theorem snopeqop

Description: Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a ⊢ 𝐴 ∈ V
snopeqop.b ⊢ 𝐵 ∈ V
Assertion snopeqop ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 snopeqop.a ⊢ 𝐴 ∈ V
2 snopeqop.b ⊢ 𝐵 ∈ V
3 eqcom ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = { ⟨ 𝐴 , 𝐵 ⟩ } )
4 opeqsng ⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( ⟨ 𝐶 , 𝐷 ⟩ = { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ( 𝐶 = 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ) ) )
5 4 ancoms ⊢ ( ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( ⟨ 𝐶 , 𝐷 ⟩ = { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ( 𝐶 = 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ) ) )
6 3 5 bitrid ⊢ ( ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐶 = 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ) ) )
7 1 2 opeqsn ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) )
8 7 a1i ⊢ ( ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) )
9 8 anbi2d ⊢ ( ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝐶 = 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ) ↔ ( 𝐶 = 𝐷 ∧ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) ) )
10 3anan12 ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ↔ ( 𝐶 = 𝐷 ∧ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) )
11 10 bicomi ⊢ ( ( 𝐶 = 𝐷 ∧ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) )
12 11 a1i ⊢ ( ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝐶 = 𝐷 ∧ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
13 6 9 12 3bitrd ⊢ ( ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
14 opprc2 ⊢ ( ¬ 𝐷 ∈ V → ⟨ 𝐶 , 𝐷 ⟩ = ∅ )
15 14 eqeq2d ⊢ ( ¬ 𝐷 ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ ) )
16 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
17 16 snnz ⊢ { ⟨ 𝐴 , 𝐵 ⟩ } ≠ ∅
18 eqneqall ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ → ( { ⟨ 𝐴 , 𝐵 ⟩ } ≠ ∅ → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
19 17 18 mpi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) )
20 15 19 syl6bi ⊢ ( ¬ 𝐷 ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
21 20 adantr ⊢ ( ( ¬ 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
22 eleq1 ⊢ ( 𝐷 = 𝐶 → ( 𝐷 ∈ V ↔ 𝐶 ∈ V ) )
23 22 notbid ⊢ ( 𝐷 = 𝐶 → ( ¬ 𝐷 ∈ V ↔ ¬ 𝐶 ∈ V ) )
24 23 eqcoms ⊢ ( 𝐶 = 𝐷 → ( ¬ 𝐷 ∈ V ↔ ¬ 𝐶 ∈ V ) )
25 pm2.21 ⊢ ( ¬ 𝐶 ∈ V → ( 𝐶 ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
26 24 25 syl6bi ⊢ ( 𝐶 = 𝐷 → ( ¬ 𝐷 ∈ V → ( 𝐶 ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) ) )
27 26 impd ⊢ ( 𝐶 = 𝐷 → ( ( ¬ 𝐷 ∈ V ∧ 𝐶 ∈ V ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
28 27 3ad2ant2 ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) → ( ( ¬ 𝐷 ∈ V ∧ 𝐶 ∈ V ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
29 28 com12 ⊢ ( ( ¬ 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
30 21 29 impbid ⊢ ( ( ¬ 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
31 13 30 pm2.61ian ⊢ ( 𝐶 ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
32 opprc1 ⊢ ( ¬ 𝐶 ∈ V → ⟨ 𝐶 , 𝐷 ⟩ = ∅ )
33 32 eqeq2d ⊢ ( ¬ 𝐶 ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ ) )
34 33 19 syl6bi ⊢ ( ¬ 𝐶 ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
35 eleq1 ⊢ ( 𝐶 = { 𝐴 } → ( 𝐶 ∈ V ↔ { 𝐴 } ∈ V ) )
36 35 notbid ⊢ ( 𝐶 = { 𝐴 } → ( ¬ 𝐶 ∈ V ↔ ¬ { 𝐴 } ∈ V ) )
37 snex ⊢ { 𝐴 } ∈ V
38 37 pm2.24i ⊢ ( ¬ { 𝐴 } ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ )
39 36 38 syl6bi ⊢ ( 𝐶 = { 𝐴 } → ( ¬ 𝐶 ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
40 39 3ad2ant3 ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) → ( ¬ 𝐶 ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
41 40 com12 ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ) )
42 34 41 impbid ⊢ ( ¬ 𝐶 ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) ) )
43 31 42 pm2.61i ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = { 𝐴 } ) )