Metamath Proof Explorer

Theorem opthwiener

Description: Justification theorem for the ordered pair definition in Norbert Wiener, A simplification of the logic of relations, Proceedings of the Cambridge Philosophical Society, 1914, vol. 17, pp.387-390. It is also shown as a definition in Enderton p. 36 and as Exercise 4.8(b) of Mendelson p. 230. It is meaningful only for classes that exist as sets (i.e., are not proper classes). See df-op for other ordered pair definitions. (Contributed by NM, 28-Sep-2003)

Ref Expression
Hypotheses opthw.1 ⊢ 𝐴 ∈ V
opthw.2 ⊢ 𝐵 ∈ V
Assertion opthwiener ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 opthw.1 ⊢ 𝐴 ∈ V
2 opthw.2 ⊢ 𝐵 ∈ V
3 id ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } )
4 snex ⊢ { { 𝐵 } } ∈ V
5 4 prid2 ⊢ { { 𝐵 } } ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } }
6 eleq2 ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → ( { { 𝐵 } } ∈ { { { 𝐴 } , ∅ } , { { 𝐵 } } } ↔ { { 𝐵 } } ∈ { { { 𝐶 } , ∅ } , { { 𝐷 } } } ) )
7 5 6 mpbii ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { { 𝐵 } } ∈ { { { 𝐶 } , ∅ } , { { 𝐷 } } } )
8 4 elpr ⊢ ( { { 𝐵 } } ∈ { { { 𝐶 } , ∅ } , { { 𝐷 } } } ↔ ( { { 𝐵 } } = { { 𝐶 } , ∅ } ∨ { { 𝐵 } } = { { 𝐷 } } ) )
9 7 8 sylib ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → ( { { 𝐵 } } = { { 𝐶 } , ∅ } ∨ { { 𝐵 } } = { { 𝐷 } } ) )
10 0ex ⊢ ∅ ∈ V
11 10 prid2 ⊢ ∅ ∈ { { 𝐶 } , ∅ }
12 2 snnz ⊢ { 𝐵 } ≠ ∅
13 10 elsn ⊢ ( ∅ ∈ { { 𝐵 } } ↔ ∅ = { 𝐵 } )
14 eqcom ⊢ ( ∅ = { 𝐵 } ↔ { 𝐵 } = ∅ )
15 13 14 bitri ⊢ ( ∅ ∈ { { 𝐵 } } ↔ { 𝐵 } = ∅ )
16 12 15 nemtbir ⊢ ¬ ∅ ∈ { { 𝐵 } }
17 nelneq2 ⊢ ( ( ∅ ∈ { { 𝐶 } , ∅ } ∧ ¬ ∅ ∈ { { 𝐵 } } ) → ¬ { { 𝐶 } , ∅ } = { { 𝐵 } } )
18 11 16 17 mp2an ⊢ ¬ { { 𝐶 } , ∅ } = { { 𝐵 } }
19 eqcom ⊢ ( { { 𝐶 } , ∅ } = { { 𝐵 } } ↔ { { 𝐵 } } = { { 𝐶 } , ∅ } )
20 18 19 mtbi ⊢ ¬ { { 𝐵 } } = { { 𝐶 } , ∅ }
21 biorf ⊢ ( ¬ { { 𝐵 } } = { { 𝐶 } , ∅ } → ( { { 𝐵 } } = { { 𝐷 } } ↔ ( { { 𝐵 } } = { { 𝐶 } , ∅ } ∨ { { 𝐵 } } = { { 𝐷 } } ) ) )
22 20 21 ax-mp ⊢ ( { { 𝐵 } } = { { 𝐷 } } ↔ ( { { 𝐵 } } = { { 𝐶 } , ∅ } ∨ { { 𝐵 } } = { { 𝐷 } } ) )
23 9 22 sylibr ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { { 𝐵 } } = { { 𝐷 } } )
24 23 preq2d ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { { { 𝐶 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } )
25 3 24 eqtr4d ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐵 } } } )
26 prex ⊢ { { 𝐴 } , ∅ } ∈ V
27 prex ⊢ { { 𝐶 } , ∅ } ∈ V
28 26 27 preqr1 ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐵 } } } → { { 𝐴 } , ∅ } = { { 𝐶 } , ∅ } )
29 25 28 syl ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { { 𝐴 } , ∅ } = { { 𝐶 } , ∅ } )
30 snex ⊢ { 𝐴 } ∈ V
31 snex ⊢ { 𝐶 } ∈ V
32 30 31 preqr1 ⊢ ( { { 𝐴 } , ∅ } = { { 𝐶 } , ∅ } → { 𝐴 } = { 𝐶 } )
33 29 32 syl ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { 𝐴 } = { 𝐶 } )
34 1 sneqr ⊢ ( { 𝐴 } = { 𝐶 } → 𝐴 = 𝐶 )
35 33 34 syl ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → 𝐴 = 𝐶 )
36 snex ⊢ { 𝐵 } ∈ V
37 36 sneqr ⊢ ( { { 𝐵 } } = { { 𝐷 } } → { 𝐵 } = { 𝐷 } )
38 23 37 syl ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → { 𝐵 } = { 𝐷 } )
39 2 sneqr ⊢ ( { 𝐵 } = { 𝐷 } → 𝐵 = 𝐷 )
40 38 39 syl ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → 𝐵 = 𝐷 )
41 35 40 jca ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
42 sneq ⊢ ( 𝐴 = 𝐶 → { 𝐴 } = { 𝐶 } )
43 42 preq1d ⊢ ( 𝐴 = 𝐶 → { { 𝐴 } , ∅ } = { { 𝐶 } , ∅ } )
44 43 preq1d ⊢ ( 𝐴 = 𝐶 → { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐵 } } } )
45 sneq ⊢ ( 𝐵 = 𝐷 → { 𝐵 } = { 𝐷 } )
46 sneq ⊢ ( { 𝐵 } = { 𝐷 } → { { 𝐵 } } = { { 𝐷 } } )
47 45 46 syl ⊢ ( 𝐵 = 𝐷 → { { 𝐵 } } = { { 𝐷 } } )
48 47 preq2d ⊢ ( 𝐵 = 𝐷 → { { { 𝐶 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } )
49 44 48 sylan9eq ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } )
50 41 49 impbii ⊢ ( { { { 𝐴 } , ∅ } , { { 𝐵 } } } = { { { 𝐶 } , ∅ } , { { 𝐷 } } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )