This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opthprc

Description: Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in Jech p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003)

Ref Expression
Assertion opthprc 
|- ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( <. x , (/) >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) <-> <. x , (/) >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) ) )
2 0ex 
 |-  (/) e. _V
3 2 snid 
 |-  (/) e. { (/) }
4 opelxp 
 |-  ( <. x , (/) >. e. ( A X. { (/) } ) <-> ( x e. A /\ (/) e. { (/) } ) )
5 3 4 mpbiran2 
 |-  ( <. x , (/) >. e. ( A X. { (/) } ) <-> x e. A )
6 opelxp 
 |-  ( <. x , (/) >. e. ( B X. { { (/) } } ) <-> ( x e. B /\ (/) e. { { (/) } } ) )
7 0nep0 
 |-  (/) =/= { (/) }
8 2 elsn 
 |-  ( (/) e. { { (/) } } <-> (/) = { (/) } )
9 7 8 nemtbir 
 |-  -. (/) e. { { (/) } }
10 9 bianfi 
 |-  ( (/) e. { { (/) } } <-> ( x e. B /\ (/) e. { { (/) } } ) )
11 6 10 bitr4i 
 |-  ( <. x , (/) >. e. ( B X. { { (/) } } ) <-> (/) e. { { (/) } } )
12 5 11 orbi12i 
 |-  ( ( <. x , (/) >. e. ( A X. { (/) } ) \/ <. x , (/) >. e. ( B X. { { (/) } } ) ) <-> ( x e. A \/ (/) e. { { (/) } } ) )
13 elun 
 |-  ( <. x , (/) >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) <-> ( <. x , (/) >. e. ( A X. { (/) } ) \/ <. x , (/) >. e. ( B X. { { (/) } } ) ) )
14 9 biorfri 
 |-  ( x e. A <-> ( x e. A \/ (/) e. { { (/) } } ) )
15 12 13 14 3bitr4ri 
 |-  ( x e. A <-> <. x , (/) >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) )
16 opelxp 
 |-  ( <. x , (/) >. e. ( C X. { (/) } ) <-> ( x e. C /\ (/) e. { (/) } ) )
17 3 16 mpbiran2 
 |-  ( <. x , (/) >. e. ( C X. { (/) } ) <-> x e. C )
18 opelxp 
 |-  ( <. x , (/) >. e. ( D X. { { (/) } } ) <-> ( x e. D /\ (/) e. { { (/) } } ) )
19 9 bianfi 
 |-  ( (/) e. { { (/) } } <-> ( x e. D /\ (/) e. { { (/) } } ) )
20 18 19 bitr4i 
 |-  ( <. x , (/) >. e. ( D X. { { (/) } } ) <-> (/) e. { { (/) } } )
21 17 20 orbi12i 
 |-  ( ( <. x , (/) >. e. ( C X. { (/) } ) \/ <. x , (/) >. e. ( D X. { { (/) } } ) ) <-> ( x e. C \/ (/) e. { { (/) } } ) )
22 elun 
 |-  ( <. x , (/) >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( <. x , (/) >. e. ( C X. { (/) } ) \/ <. x , (/) >. e. ( D X. { { (/) } } ) ) )
23 9 biorfri 
 |-  ( x e. C <-> ( x e. C \/ (/) e. { { (/) } } ) )
24 21 22 23 3bitr4ri 
 |-  ( x e. C <-> <. x , (/) >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
25 1 15 24 3bitr4g 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( x e. A <-> x e. C ) )
26 25 eqrdv 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> A = C )
27 eleq2 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( <. x , { (/) } >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) <-> <. x , { (/) } >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) ) )
28 opelxp 
 |-  ( <. x , { (/) } >. e. ( A X. { (/) } ) <-> ( x e. A /\ { (/) } e. { (/) } ) )
29 snex 
 |-  { (/) } e. _V
30 29 elsn 
 |-  ( { (/) } e. { (/) } <-> { (/) } = (/) )
31 eqcom 
 |-  ( { (/) } = (/) <-> (/) = { (/) } )
32 30 31 bitri 
 |-  ( { (/) } e. { (/) } <-> (/) = { (/) } )
33 7 32 nemtbir 
 |-  -. { (/) } e. { (/) }
34 33 bianfi 
 |-  ( { (/) } e. { (/) } <-> ( x e. A /\ { (/) } e. { (/) } ) )
35 28 34 bitr4i 
 |-  ( <. x , { (/) } >. e. ( A X. { (/) } ) <-> { (/) } e. { (/) } )
36 29 snid 
 |-  { (/) } e. { { (/) } }
37 opelxp 
 |-  ( <. x , { (/) } >. e. ( B X. { { (/) } } ) <-> ( x e. B /\ { (/) } e. { { (/) } } ) )
38 36 37 mpbiran2 
 |-  ( <. x , { (/) } >. e. ( B X. { { (/) } } ) <-> x e. B )
39 35 38 orbi12i 
 |-  ( ( <. x , { (/) } >. e. ( A X. { (/) } ) \/ <. x , { (/) } >. e. ( B X. { { (/) } } ) ) <-> ( { (/) } e. { (/) } \/ x e. B ) )
40 elun 
 |-  ( <. x , { (/) } >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) <-> ( <. x , { (/) } >. e. ( A X. { (/) } ) \/ <. x , { (/) } >. e. ( B X. { { (/) } } ) ) )
41 33 biorfi 
 |-  ( x e. B <-> ( { (/) } e. { (/) } \/ x e. B ) )
42 39 40 41 3bitr4ri 
 |-  ( x e. B <-> <. x , { (/) } >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) )
43 opelxp 
 |-  ( <. x , { (/) } >. e. ( C X. { (/) } ) <-> ( x e. C /\ { (/) } e. { (/) } ) )
44 33 bianfi 
 |-  ( { (/) } e. { (/) } <-> ( x e. C /\ { (/) } e. { (/) } ) )
45 43 44 bitr4i 
 |-  ( <. x , { (/) } >. e. ( C X. { (/) } ) <-> { (/) } e. { (/) } )
46 opelxp 
 |-  ( <. x , { (/) } >. e. ( D X. { { (/) } } ) <-> ( x e. D /\ { (/) } e. { { (/) } } ) )
47 36 46 mpbiran2 
 |-  ( <. x , { (/) } >. e. ( D X. { { (/) } } ) <-> x e. D )
48 45 47 orbi12i 
 |-  ( ( <. x , { (/) } >. e. ( C X. { (/) } ) \/ <. x , { (/) } >. e. ( D X. { { (/) } } ) ) <-> ( { (/) } e. { (/) } \/ x e. D ) )
49 elun 
 |-  ( <. x , { (/) } >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( <. x , { (/) } >. e. ( C X. { (/) } ) \/ <. x , { (/) } >. e. ( D X. { { (/) } } ) ) )
50 33 biorfi 
 |-  ( x e. D <-> ( { (/) } e. { (/) } \/ x e. D ) )
51 48 49 50 3bitr4ri 
 |-  ( x e. D <-> <. x , { (/) } >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
52 27 42 51 3bitr4g 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( x e. B <-> x e. D ) )
53 52 eqrdv 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> B = D )
54 26 53 jca 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( A = C /\ B = D ) )
55 xpeq1 
 |-  ( A = C -> ( A X. { (/) } ) = ( C X. { (/) } ) )
56 xpeq1 
 |-  ( B = D -> ( B X. { { (/) } } ) = ( D X. { { (/) } } ) )
57 uneq12 
 |-  ( ( ( A X. { (/) } ) = ( C X. { (/) } ) /\ ( B X. { { (/) } } ) = ( D X. { { (/) } } ) ) -> ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
58 55 56 57 syl2an 
 |-  ( ( A = C /\ B = D ) -> ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
59 54 58 impbii 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( A = C /\ B = D ) )