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 × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅ ↔ A = C ∧ B = D

Proof

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