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 
|- A e. _V
opthw.2 
|- B e. _V
Assertion opthwiener 
|- ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } <-> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 opthw.1 
 |-  A e. _V
2 opthw.2 
 |-  B e. _V
3 id 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } )
4 snex 
 |-  { { B } } e. _V
5 4 prid2 
 |-  { { B } } e. { { { A } , (/) } , { { B } } }
6 eleq2 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> ( { { B } } e. { { { A } , (/) } , { { B } } } <-> { { B } } e. { { { C } , (/) } , { { D } } } ) )
7 5 6 mpbii 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { { B } } e. { { { C } , (/) } , { { D } } } )
8 4 elpr 
 |-  ( { { B } } e. { { { C } , (/) } , { { D } } } <-> ( { { B } } = { { C } , (/) } \/ { { B } } = { { D } } ) )
9 7 8 sylib 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> ( { { B } } = { { C } , (/) } \/ { { B } } = { { D } } ) )
10 0ex 
 |-  (/) e. _V
11 10 prid2 
 |-  (/) e. { { C } , (/) }
12 2 snnz 
 |-  { B } =/= (/)
13 10 elsn 
 |-  ( (/) e. { { B } } <-> (/) = { B } )
14 eqcom 
 |-  ( (/) = { B } <-> { B } = (/) )
15 13 14 bitri 
 |-  ( (/) e. { { B } } <-> { B } = (/) )
16 12 15 nemtbir 
 |-  -. (/) e. { { B } }
17 nelneq2 
 |-  ( ( (/) e. { { C } , (/) } /\ -. (/) e. { { B } } ) -> -. { { C } , (/) } = { { B } } )
18 11 16 17 mp2an 
 |-  -. { { C } , (/) } = { { B } }
19 eqcom 
 |-  ( { { C } , (/) } = { { B } } <-> { { B } } = { { C } , (/) } )
20 18 19 mtbi 
 |-  -. { { B } } = { { C } , (/) }
21 biorf 
 |-  ( -. { { B } } = { { C } , (/) } -> ( { { B } } = { { D } } <-> ( { { B } } = { { C } , (/) } \/ { { B } } = { { D } } ) ) )
22 20 21 ax-mp 
 |-  ( { { B } } = { { D } } <-> ( { { B } } = { { C } , (/) } \/ { { B } } = { { D } } ) )
23 9 22 sylibr 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { { B } } = { { D } } )
24 23 preq2d 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { { { C } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } )
25 3 24 eqtr4d 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { B } } } )
26 prex 
 |-  { { A } , (/) } e. _V
27 prex 
 |-  { { C } , (/) } e. _V
28 26 27 preqr1 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { B } } } -> { { A } , (/) } = { { C } , (/) } )
29 25 28 syl 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { { A } , (/) } = { { C } , (/) } )
30 snex 
 |-  { A } e. _V
31 snex 
 |-  { C } e. _V
32 30 31 preqr1 
 |-  ( { { A } , (/) } = { { C } , (/) } -> { A } = { C } )
33 29 32 syl 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { A } = { C } )
34 1 sneqr 
 |-  ( { A } = { C } -> A = C )
35 33 34 syl 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> A = C )
36 snex 
 |-  { B } e. _V
37 36 sneqr 
 |-  ( { { B } } = { { D } } -> { B } = { D } )
38 23 37 syl 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> { B } = { D } )
39 2 sneqr 
 |-  ( { B } = { D } -> B = D )
40 38 39 syl 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> B = D )
41 35 40 jca 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } -> ( A = C /\ B = D ) )
42 sneq 
 |-  ( A = C -> { A } = { C } )
43 42 preq1d 
 |-  ( A = C -> { { A } , (/) } = { { C } , (/) } )
44 43 preq1d 
 |-  ( A = C -> { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { B } } } )
45 sneq 
 |-  ( B = D -> { B } = { D } )
46 sneq 
 |-  ( { B } = { D } -> { { B } } = { { D } } )
47 45 46 syl 
 |-  ( B = D -> { { B } } = { { D } } )
48 47 preq2d 
 |-  ( B = D -> { { { C } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } )
49 44 48 sylan9eq 
 |-  ( ( A = C /\ B = D ) -> { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } )
50 41 49 impbii 
 |-  ( { { { A } , (/) } , { { B } } } = { { { C } , (/) } , { { D } } } <-> ( A = C /\ B = D ) )