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	biorfi	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∨ ∅ ∈ { { ∅ } } ) )
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	biorfi	⊢ ( 𝑥 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐶 ∨ ∅ ∈ { { ∅ } } ) )
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		biorf	⊢ ( ¬ { ∅ } ∈ { ∅ } → ( 𝑥 ∈ 𝐵 ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥 ∈ 𝐵 ) ) )
42	33 41	ax-mp	⊢ ( 𝑥 ∈ 𝐵 ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥 ∈ 𝐵 ) )
43	39 40 42	3bitr4ri	⊢ ( 𝑥 ∈ 𝐵 ↔ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) )
44		opelxp	⊢ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ↔ ( 𝑥 ∈ 𝐶 ∧ { ∅ } ∈ { ∅ } ) )
45	33	bianfi	⊢ ( { ∅ } ∈ { ∅ } ↔ ( 𝑥 ∈ 𝐶 ∧ { ∅ } ∈ { ∅ } ) )
46	44 45	bitr4i	⊢ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ↔ { ∅ } ∈ { ∅ } )
47		opelxp	⊢ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ↔ ( 𝑥 ∈ 𝐷 ∧ { ∅ } ∈ { { ∅ } } ) )
48	36 47	mpbiran2	⊢ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ↔ 𝑥 ∈ 𝐷 )
49	46 48	orbi12i	⊢ ( ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ∨ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ) ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥 ∈ 𝐷 ) )
50		elun	⊢ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ↔ ( ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐶 × { ∅ } ) ∨ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( 𝐷 × { { ∅ } } ) ) )
51		biorf	⊢ ( ¬ { ∅ } ∈ { ∅ } → ( 𝑥 ∈ 𝐷 ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥 ∈ 𝐷 ) ) )
52	33 51	ax-mp	⊢ ( 𝑥 ∈ 𝐷 ↔ ( { ∅ } ∈ { ∅ } ∨ 𝑥 ∈ 𝐷 ) )
53	49 50 52	3bitr4ri	⊢ ( 𝑥 ∈ 𝐷 ↔ ⟨ 𝑥 , { ∅ } ⟩ ∈ ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
54	27 43 53	3bitr4g	⊢ ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐷 ) )
55	54	eqrdv	⊢ ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → 𝐵 = 𝐷 )
56	26 55	jca	⊢ ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
57		xpeq1	⊢ ( 𝐴 = 𝐶 → ( 𝐴 × { ∅ } ) = ( 𝐶 × { ∅ } ) )
58		xpeq1	⊢ ( 𝐵 = 𝐷 → ( 𝐵 × { { ∅ } } ) = ( 𝐷 × { { ∅ } } ) )
59		uneq12	⊢ ( ( ( 𝐴 × { ∅ } ) = ( 𝐶 × { ∅ } ) ∧ ( 𝐵 × { { ∅ } } ) = ( 𝐷 × { { ∅ } } ) ) → ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
60	57 58 59	syl2an	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) )
61	56 60	impbii	⊢ ( ( ( 𝐴 × { ∅ } ) ∪ ( 𝐵 × { { ∅ } } ) ) = ( ( 𝐶 × { ∅ } ) ∪ ( 𝐷 × { { ∅ } } ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )