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

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