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 biorfri ⊢ 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 biorfri ⊢ 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 33 biorfi ⊢ x ∈ B ↔ ∅ ∈ ∅ ∨ x ∈ B
42 39 40 41 3bitr4ri ⊢ x ∈ B ↔ x ∅ ∈ A × ∅ ∪ B × ∅
43 opelxp ⊢ x ∅ ∈ C × ∅ ↔ x ∈ C ∧ ∅ ∈ ∅
44 33 bianfi ⊢ ∅ ∈ ∅ ↔ x ∈ C ∧ ∅ ∈ ∅
45 43 44 bitr4i ⊢ x ∅ ∈ C × ∅ ↔ ∅ ∈ ∅
46 opelxp ⊢ x ∅ ∈ D × ∅ ↔ x ∈ D ∧ ∅ ∈ ∅
47 36 46 mpbiran2 ⊢ x ∅ ∈ D × ∅ ↔ x ∈ D
48 45 47 orbi12i ⊢ x ∅ ∈ C × ∅ ∨ x ∅ ∈ D × ∅ ↔ ∅ ∈ ∅ ∨ x ∈ D
49 elun ⊢ x ∅ ∈ C × ∅ ∪ D × ∅ ↔ x ∅ ∈ C × ∅ ∨ x ∅ ∈ D × ∅
50 33 biorfi ⊢ x ∈ D ↔ ∅ ∈ ∅ ∨ x ∈ D
51 48 49 50 3bitr4ri ⊢ x ∈ D ↔ x ∅ ∈ C × ∅ ∪ D × ∅
52 27 42 51 3bitr4g ⊢ A × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅ → x ∈ B ↔ x ∈ D
53 52 eqrdv ⊢ A × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅ → B = D
54 26 53 jca ⊢ A × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅ → A = C ∧ B = D
55 xpeq1 ⊢ A = C → A × ∅ = C × ∅
56 xpeq1 ⊢ B = D → B × ∅ = D × ∅
57 uneq12 ⊢ A × ∅ = C × ∅ ∧ B × ∅ = D × ∅ → A × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅
58 55 56 57 syl2an ⊢ A = C ∧ B = D → A × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅
59 54 58 impbii ⊢ A × ∅ ∪ B × ∅ = C × ∅ ∪ D × ∅ ↔ A = C ∧ B = D