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=CB=D

Proof

Step Hyp Ref Expression
1 eleq2 A×B×=C×D×xA×B×xC×D×
2 0ex V
3 2 snid
4 opelxp xA×xA
5 3 4 mpbiran2 xA×xA
6 opelxp xB×xB
7 0nep0
8 2 elsn =
9 7 8 nemtbir ¬
10 9 bianfi xB
11 6 10 bitr4i xB×
12 5 11 orbi12i xA×xB×xA
13 elun xA×B×xA×xB×
14 9 biorfi xAxA
15 12 13 14 3bitr4ri xAxA×B×
16 opelxp xC×xC
17 3 16 mpbiran2 xC×xC
18 opelxp xD×xD
19 9 bianfi xD
20 18 19 bitr4i xD×
21 17 20 orbi12i xC×xD×xC
22 elun xC×D×xC×xD×
23 9 biorfi xCxC
24 21 22 23 3bitr4ri xCxC×D×
25 1 15 24 3bitr4g A×B×=C×D×xAxC
26 25 eqrdv A×B×=C×D×A=C
27 eleq2 A×B×=C×D×xA×B×xC×D×
28 opelxp xA×xA
29 snex V
30 29 elsn =
31 eqcom ==
32 30 31 bitri =
33 7 32 nemtbir ¬
34 33 bianfi xA
35 28 34 bitr4i xA×
36 29 snid
37 opelxp xB×xB
38 36 37 mpbiran2 xB×xB
39 35 38 orbi12i xA×xB×xB
40 elun xA×B×xA×xB×
41 biorf ¬xBxB
42 33 41 ax-mp xBxB
43 39 40 42 3bitr4ri xBxA×B×
44 opelxp xC×xC
45 33 bianfi xC
46 44 45 bitr4i xC×
47 opelxp xD×xD
48 36 47 mpbiran2 xD×xD
49 46 48 orbi12i xC×xD×xD
50 elun xC×D×xC×xD×
51 biorf ¬xDxD
52 33 51 ax-mp xDxD
53 49 50 52 3bitr4ri xDxC×D×
54 27 43 53 3bitr4g A×B×=C×D×xBxD
55 54 eqrdv A×B×=C×D×B=D
56 26 55 jca A×B×=C×D×A=CB=D
57 xpeq1 A=CA×=C×
58 xpeq1 B=DB×=D×
59 uneq12 A×=C×B×=D×A×B×=C×D×
60 57 58 59 syl2an A=CB=DA×B×=C×D×
61 56 60 impbii A×B×=C×D×A=CB=D