Theorem opthprc 2457

Description: Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is the 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."

Assertion

Ref	Expression
opthprc	⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) ↔ (A = C ∧ B = D))

Proof of Theorem opthprc

Step	Hyp	Ref	Expression
1		eleq2 1150	. . . . 5 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → (⟨x, ∅⟩ ∈ ((A × {∅}) ∪ (B × {{∅}})) ↔ ⟨x, ∅⟩ ∈ ((C × {∅}) ∪ (D × {{∅}}))))
2		0ex 1745	. . . . . . . . 9 ⊢ ∅ ∈ V
3	2	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, ∅⟩ ∈ (A × {∅}) ↔ (x ∈ A ∧ ∅ ∈ {∅}))
4	2	snid 1830	. . . . . . . 8 ⊢ ∅ ∈ {∅}
5	3, 4	mpbiranr 548	. . . . . . 7 ⊢ (⟨x, ∅⟩ ∈ (A × {∅}) ↔ x ∈ A)
6	2	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, ∅⟩ ∈ (B × {{∅}}) ↔ (x ∈ B ∧ ∅ ∈ {{∅}}))
7		0nep0 1887	. . . . . . . . . 10 ⊢ ¬ ∅ = {∅}
8	2	elsnc 1826	. . . . . . . . . 10 ⊢ (∅ ∈ {{∅}} ↔ ∅ = {∅})
9	7, 8	mtbir 167	. . . . . . . . 9 ⊢ ¬ ∅ ∈ {{∅}}
10	9	bianfi 553	. . . . . . . 8 ⊢ (∅ ∈ {{∅}} ↔ (x ∈ B ∧ ∅ ∈ {{∅}}))
11	6, 10	bitr4 154	. . . . . . 7 ⊢ (⟨x, ∅⟩ ∈ (B × {{∅}}) ↔ ∅ ∈ {{∅}})
12	5, 11	orbi12i 216	. . . . . 6 ⊢ ((⟨x, ∅⟩ ∈ (A × {∅}) ∨ ⟨x, ∅⟩ ∈ (B × {{∅}})) ↔ (x ∈ A ∨ ∅ ∈ {{∅}}))
13		elun 1601	. . . . . 6 ⊢ (⟨x, ∅⟩ ∈ ((A × {∅}) ∪ (B × {{∅}})) ↔ (⟨x, ∅⟩ ∈ (A × {∅}) ∨ ⟨x, ∅⟩ ∈ (B × {{∅}})))
14	9	biorfi 552	. . . . . 6 ⊢ (x ∈ A ↔ (x ∈ A ∨ ∅ ∈ {{∅}}))
15	12, 13, 14	3bitr4r 159	. . . . 5 ⊢ (x ∈ A ↔ ⟨x, ∅⟩ ∈ ((A × {∅}) ∪ (B × {{∅}})))
16	2	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, ∅⟩ ∈ (C × {∅}) ↔ (x ∈ C ∧ ∅ ∈ {∅}))
17	16, 4	mpbiranr 548	. . . . . . 7 ⊢ (⟨x, ∅⟩ ∈ (C × {∅}) ↔ x ∈ C)
18	2	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, ∅⟩ ∈ (D × {{∅}}) ↔ (x ∈ D ∧ ∅ ∈ {{∅}}))
19	9	bianfi 553	. . . . . . . 8 ⊢ (∅ ∈ {{∅}} ↔ (x ∈ D ∧ ∅ ∈ {{∅}}))
20	18, 19	bitr4 154	. . . . . . 7 ⊢ (⟨x, ∅⟩ ∈ (D × {{∅}}) ↔ ∅ ∈ {{∅}})
21	17, 20	orbi12i 216	. . . . . 6 ⊢ ((⟨x, ∅⟩ ∈ (C × {∅}) ∨ ⟨x, ∅⟩ ∈ (D × {{∅}})) ↔ (x ∈ C ∨ ∅ ∈ {{∅}}))
22		elun 1601	. . . . . 6 ⊢ (⟨x, ∅⟩ ∈ ((C × {∅}) ∪ (D × {{∅}})) ↔ (⟨x, ∅⟩ ∈ (C × {∅}) ∨ ⟨x, ∅⟩ ∈ (D × {{∅}})))
23	9	biorfi 552	. . . . . 6 ⊢ (x ∈ C ↔ (x ∈ C ∨ ∅ ∈ {{∅}}))
24	21, 22, 23	3bitr4r 159	. . . . 5 ⊢ (x ∈ C ↔ ⟨x, ∅⟩ ∈ ((C × {∅}) ∪ (D × {{∅}})))
25	1, 15, 24	3bitr4g 428	. . . 4 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → (x ∈ A ↔ x ∈ C))
26	25	cleqrd 1100	. . 3 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → A = C)
27		eleq2 1150	. . . . 5 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → (⟨x, {∅}⟩ ∈ ((A × {∅}) ∪ (B × {{∅}})) ↔ ⟨x, {∅}⟩ ∈ ((C × {∅}) ∪ (D × {{∅}}))))
28		p0ex 1885	. . . . . . . . 9 ⊢ {∅} ∈ V
29	28	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, {∅}⟩ ∈ (A × {∅}) ↔ (x ∈ A ∧ {∅} ∈ {∅}))
30	28	elsnc 1826	. . . . . . . . . . 11 ⊢ ({∅} ∈ {∅} ↔ {∅} = ∅)
31		cleqcom 1103	. . . . . . . . . . 11 ⊢ ({∅} = ∅ ↔ ∅ = {∅})
32	30, 31	bitr 151	. . . . . . . . . 10 ⊢ ({∅} ∈ {∅} ↔ ∅ = {∅})
33	7, 32	mtbir 167	. . . . . . . . 9 ⊢ ¬ {∅} ∈ {∅}
34	33	bianfi 553	. . . . . . . 8 ⊢ ({∅} ∈ {∅} ↔ (x ∈ A ∧ {∅} ∈ {∅}))
35	29, 34	bitr4 154	. . . . . . 7 ⊢ (⟨x, {∅}⟩ ∈ (A × {∅}) ↔ {∅} ∈ {∅})
36	28	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, {∅}⟩ ∈ (B × {{∅}}) ↔ (x ∈ B ∧ {∅} ∈ {{∅}}))
37	28	snid 1830	. . . . . . . 8 ⊢ {∅} ∈ {{∅}}
38	36, 37	mpbiranr 548	. . . . . . 7 ⊢ (⟨x, {∅}⟩ ∈ (B × {{∅}}) ↔ x ∈ B)
39	35, 38	orbi12i 216	. . . . . 6 ⊢ ((⟨x, {∅}⟩ ∈ (A × {∅}) ∨ ⟨x, {∅}⟩ ∈ (B × {{∅}})) ↔ ({∅} ∈ {∅} ∨ x ∈ B))
40		elun 1601	. . . . . 6 ⊢ (⟨x, {∅}⟩ ∈ ((A × {∅}) ∪ (B × {{∅}})) ↔ (⟨x, {∅}⟩ ∈ (A × {∅}) ∨ ⟨x, {∅}⟩ ∈ (B × {{∅}})))
41		biorf 551	. . . . . . 7 ⊢ (¬ {∅} ∈ {∅} → (x ∈ B ↔ ({∅} ∈ {∅} ∨ x ∈ B)))
42	33, 41	ax-mp 6	. . . . . 6 ⊢ (x ∈ B ↔ ({∅} ∈ {∅} ∨ x ∈ B))
43	39, 40, 42	3bitr4r 159	. . . . 5 ⊢ (x ∈ B ↔ ⟨x, {∅}⟩ ∈ ((A × {∅}) ∪ (B × {{∅}})))
44	28	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, {∅}⟩ ∈ (C × {∅}) ↔ (x ∈ C ∧ {∅} ∈ {∅}))
45	33	bianfi 553	. . . . . . . 8 ⊢ ({∅} ∈ {∅} ↔ (x ∈ C ∧ {∅} ∈ {∅}))
46	44, 45	bitr4 154	. . . . . . 7 ⊢ (⟨x, {∅}⟩ ∈ (C × {∅}) ↔ {∅} ∈ {∅})
47	28	opelxp 2452	. . . . . . . 8 ⊢ (⟨x, {∅}⟩ ∈ (D × {{∅}}) ↔ (x ∈ D ∧ {∅} ∈ {{∅}}))
48	47, 37	mpbiranr 548	. . . . . . 7 ⊢ (⟨x, {∅}⟩ ∈ (D × {{∅}}) ↔ x ∈ D)
49	46, 48	orbi12i 216	. . . . . 6 ⊢ ((⟨x, {∅}⟩ ∈ (C × {∅}) ∨ ⟨x, {∅}⟩ ∈ (D × {{∅}})) ↔ ({∅} ∈ {∅} ∨ x ∈ D))
50		elun 1601	. . . . . 6 ⊢ (⟨x, {∅}⟩ ∈ ((C × {∅}) ∪ (D × {{∅}})) ↔ (⟨x, {∅}⟩ ∈ (C × {∅}) ∨ ⟨x, {∅}⟩ ∈ (D × {{∅}})))
51		biorf 551	. . . . . . 7 ⊢ (¬ {∅} ∈ {∅} → (x ∈ D ↔ ({∅} ∈ {∅} ∨ x ∈ D)))
52	33, 51	ax-mp 6	. . . . . 6 ⊢ (x ∈ D ↔ ({∅} ∈ {∅} ∨ x ∈ D))
53	49, 50, 52	3bitr4r 159	. . . . 5 ⊢ (x ∈ D ↔ ⟨x, {∅}⟩ ∈ ((C × {∅}) ∪ (D × {{∅}})))
54	27, 43, 53	3bitr4g 428	. . . 4 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → (x ∈ B ↔ x ∈ D))
55	54	cleqrd 1100	. . 3 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → B = D)
56	26, 55	jca 236	. 2 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) → (A = C ∧ B = D))
57		uneq12 1613	. . 3 ⊢ (((A × {∅}) = (C × {∅}) ∧ (B × {{∅}}) = (D × {{∅}})) → ((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})))
58		xpeq1 2440	. . 3 ⊢ (A = C → (A × {∅}) = (C × {∅}))
59		xpeq1 2440	. . 3 ⊢ (B = D → (B × {{∅}}) = (D × {{∅}}))
60	57, 58, 59	syl2an 349	. 2 ⊢ ((A = C ∧ B = D) → ((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})))
61	56, 60	impbi 139	1 ⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) ↔ (A = C ∧ B = D))

Syntax hints:  ¬ wn 1   ↔ wb 127   ∨ wo 195   ∧ wa 196   = wceq 1091   ∈ wcel 1092   ∪ cun 1485  ∅c0 1707  {csn 1808  ⟨cop 1810   × cxp 2408

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-opab 2098  df-xp 2424

metamath.org