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 ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 eleq2 ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ) )
2 0ex ∅ ∈ V
3 2 snid ∅ ∈ { ∅ }
4 opelxp ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐴 × { ∅ } ) ↔ ( 𝑥𝐴 ∧ ∅ ∈ { ∅ } ) )
5 3 4 mpbiran2 ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐴 × { ∅ } ) ↔ 𝑥𝐴 )
6 opelxp ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐵 × { { ∅ } } ) ↔ ( 𝑥𝐵 ∧ ∅ ∈ { { ∅ } } ) )
7 0nep0 ∅ ≠ { ∅ }
8 2 elsn ( ∅ ∈ { { ∅ } } ↔ ∅ = { ∅ } )
9 7 8 nemtbir ¬ ∅ ∈ { { ∅ } }
10 9 bianfi ( ∅ ∈ { { ∅ } } ↔ ( 𝑥𝐵 ∧ ∅ ∈ { { ∅ } } ) )
11 6 10 bitr4i ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐵 × { { ∅ } } ) ↔ ∅ ∈ { { ∅ } } )
12 5 11 orbi12i ( ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐴 × { ∅ } ) ∨ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐵 × { { ∅ } } ) ) ↔ ( 𝑥𝐴 ∨ ∅ ∈ { { ∅ } } ) )
13 elun ( ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) ↔ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐴 × { ∅ } ) ∨ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐵 × { { ∅ } } ) ) )
14 9 biorfri ( 𝑥𝐴 ↔ ( 𝑥𝐴 ∨ ∅ ∈ { { ∅ } } ) )
15 12 13 14 3bitr4ri ( 𝑥𝐴 ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) )
16 opelxp ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐶 × { ∅ } ) ↔ ( 𝑥𝐶 ∧ ∅ ∈ { ∅ } ) )
17 3 16 mpbiran2 ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐶 × { ∅ } ) ↔ 𝑥𝐶 )
18 opelxp ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐷 × { { ∅ } } ) ↔ ( 𝑥𝐷 ∧ ∅ ∈ { { ∅ } } ) )
19 9 bianfi ( ∅ ∈ { { ∅ } } ↔ ( 𝑥𝐷 ∧ ∅ ∈ { { ∅ } } ) )
20 18 19 bitr4i ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐷 × { { ∅ } } ) ↔ ∅ ∈ { { ∅ } } )
21 17 20 orbi12i ( ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐶 × { ∅ } ) ∨ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐷 × { { ∅ } } ) ) ↔ ( 𝑥𝐶 ∨ ∅ ∈ { { ∅ } } ) )
22 elun ( ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ↔ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐶 × { ∅ } ) ∨ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝐷 × { { ∅ } } ) ) )
23 9 biorfri ( 𝑥𝐶 ↔ ( 𝑥𝐶 ∨ ∅ ∈ { { ∅ } } ) )
24 21 22 23 3bitr4ri ( 𝑥𝐶 ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
25 1 15 24 3bitr4g ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( 𝑥𝐴𝑥𝐶 ) )
26 25 eqrdv ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → 𝐴 = 𝐶 )
27 eleq2 ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) ↔ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ) )
28 opelxp ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐴 × { ∅ } ) ↔ ( 𝑥𝐴 ∧ { ∅ } ∈ { ∅ } ) )
29 snex { ∅ } ∈ V
30 29 elsn ( { ∅ } ∈ { ∅ } ↔ { ∅ } = ∅ )
31 eqcom ( { ∅ } = ∅ ↔ ∅ = { ∅ } )
32 30 31 bitri ( { ∅ } ∈ { ∅ } ↔ ∅ = { ∅ } )
33 7 32 nemtbir ¬ { ∅ } ∈ { ∅ }
34 33 bianfi ( { ∅ } ∈ { ∅ } ↔ ( 𝑥𝐴 ∧ { ∅ } ∈ { ∅ } ) )
35 28 34 bitr4i ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐴 × { ∅ } ) ↔ { ∅ } ∈ { ∅ } )
36 29 snid { ∅ } ∈ { { ∅ } }
37 opelxp ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐵 × { { ∅ } } ) ↔ ( 𝑥𝐵 ∧ { ∅ } ∈ { { ∅ } } ) )
38 36 37 mpbiran2 ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐵 × { { ∅ } } ) ↔ 𝑥𝐵 )
39 35 38 orbi12i ( ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐴 × { ∅ } ) ∨ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐵 × { { ∅ } } ) ) ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥𝐵 ) )
40 elun ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) ↔ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐴 × { ∅ } ) ∨ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐵 × { { ∅ } } ) ) )
41 33 biorfi ( 𝑥𝐵 ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥𝐵 ) )
42 39 40 41 3bitr4ri ( 𝑥𝐵 ↔ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) )
43 opelxp ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ↔ ( 𝑥𝐶 ∧ { ∅ } ∈ { ∅ } ) )
44 33 bianfi ( { ∅ } ∈ { ∅ } ↔ ( 𝑥𝐶 ∧ { ∅ } ∈ { ∅ } ) )
45 43 44 bitr4i ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ↔ { ∅ } ∈ { ∅ } )
46 opelxp ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ↔ ( 𝑥𝐷 ∧ { ∅ } ∈ { { ∅ } } ) )
47 36 46 mpbiran2 ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ↔ 𝑥𝐷 )
48 45 47 orbi12i ( ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ∨ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ) ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥𝐷 ) )
49 elun ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ↔ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ∨ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ) )
50 33 biorfi ( 𝑥𝐷 ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥𝐷 ) )
51 48 49 50 3bitr4ri ( 𝑥𝐷 ↔ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
52 27 42 51 3bitr4g ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( 𝑥𝐵𝑥𝐷 ) )
53 52 eqrdv ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → 𝐵 = 𝐷 )
54 26 53 jca ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )
55 xpeq1 ( 𝐴 = 𝐶 → ( 𝐴 × { ∅ } ) = ( 𝐶 × { ∅ } ) )
56 xpeq1 ( 𝐵 = 𝐷 → ( 𝐵 × { { ∅ } } ) = ( 𝐷 × { { ∅ } } ) )
57 uneq12 ( ( ( 𝐴 × { ∅ } ) = ( 𝐶 × { ∅ } ) ∧ ( 𝐵 × { { ∅ } } ) = ( 𝐷 × { { ∅ } } ) ) → ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
58 55 56 57 syl2an ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
59 54 58 impbii ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )