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 biorfi 
 |-  ( 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 biorfi 
 |-  ( 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 biorf 
 |-  ( -. { (/) } e. { (/) } -> ( x e. B <-> ( { (/) } e. { (/) } \/ x e. B ) ) )
42 33 41 ax-mp 
 |-  ( x e. B <-> ( { (/) } e. { (/) } \/ x e. B ) )
43 39 40 42 3bitr4ri 
 |-  ( x e. B <-> <. x , { (/) } >. e. ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) )
44 opelxp 
 |-  ( <. x , { (/) } >. e. ( C X. { (/) } ) <-> ( x e. C /\ { (/) } e. { (/) } ) )
45 33 bianfi 
 |-  ( { (/) } e. { (/) } <-> ( x e. C /\ { (/) } e. { (/) } ) )
46 44 45 bitr4i 
 |-  ( <. x , { (/) } >. e. ( C X. { (/) } ) <-> { (/) } e. { (/) } )
47 opelxp 
 |-  ( <. x , { (/) } >. e. ( D X. { { (/) } } ) <-> ( x e. D /\ { (/) } e. { { (/) } } ) )
48 36 47 mpbiran2 
 |-  ( <. x , { (/) } >. e. ( D X. { { (/) } } ) <-> x e. D )
49 46 48 orbi12i 
 |-  ( ( <. x , { (/) } >. e. ( C X. { (/) } ) \/ <. x , { (/) } >. e. ( D X. { { (/) } } ) ) <-> ( { (/) } e. { (/) } \/ x e. D ) )
50 elun 
 |-  ( <. x , { (/) } >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( <. x , { (/) } >. e. ( C X. { (/) } ) \/ <. x , { (/) } >. e. ( D X. { { (/) } } ) ) )
51 biorf 
 |-  ( -. { (/) } e. { (/) } -> ( x e. D <-> ( { (/) } e. { (/) } \/ x e. D ) ) )
52 33 51 ax-mp 
 |-  ( x e. D <-> ( { (/) } e. { (/) } \/ x e. D ) )
53 49 50 52 3bitr4ri 
 |-  ( x e. D <-> <. x , { (/) } >. e. ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
54 27 43 53 3bitr4g 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( x e. B <-> x e. D ) )
55 54 eqrdv 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> B = D )
56 26 55 jca 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) -> ( A = C /\ B = D ) )
57 xpeq1 
 |-  ( A = C -> ( A X. { (/) } ) = ( C X. { (/) } ) )
58 xpeq1 
 |-  ( B = D -> ( B X. { { (/) } } ) = ( D X. { { (/) } } ) )
59 uneq12 
 |-  ( ( ( A X. { (/) } ) = ( C X. { (/) } ) /\ ( B X. { { (/) } } ) = ( D X. { { (/) } } ) ) -> ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
60 57 58 59 syl2an 
 |-  ( ( A = C /\ B = D ) -> ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) )
61 56 60 impbii 
 |-  ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( A = C /\ B = D ) )