Theorem opthprc 3306

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."

Assertion

Ref	Expression
opthprc	|- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) <-> (A = C /\ B = D))

Proof of Theorem opthprc

Step	Hyp	Ref	Expression
1		eleq2 1578	. . . . 5 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (<.x, (/)>. e. ((A X. {(/)}) u. (B X. {{(/)}})) <-> <.x, (/)>. e. ((C X. {(/)}) u. (D X. {{(/)}}))))
2		0ex 2785	. . . . . . . . 9 |- (/) e. V
3	2	opelxp 3297	. . . . . . . 8 |- (<.x, (/)>. e. (A X. {(/)}) <-> (x e. A /\ (/) e. {(/)}))
4	2	snid 2496	. . . . . . . 8 |- (/) e. {(/)}
5	3, 4	mpbiran2 734	. . . . . . 7 |- (<.x, (/)>. e. (A X. {(/)}) <-> x e. A)
6	2	opelxp 3297	. . . . . . . 8 |- (<.x, (/)>. e. (B X. {{(/)}}) <-> (x e. B /\ (/) e. {{(/)}}))
7		0nep0 2811	. . . . . . . . . 10 |- (/) =/= {(/)}
8	2	elsnc 2492	. . . . . . . . . 10 |- ((/) e. {{(/)}} <-> (/) = {(/)})
9	7, 8	nemtbir 1687	. . . . . . . . 9 |- -. (/) e. {{(/)}}
10	9	bianfi 742	. . . . . . . 8 |- ((/) e. {{(/)}} <-> (x e. B /\ (/) e. {{(/)}}))
11	6, 10	bitr4i 174	. . . . . . 7 |- (<.x, (/)>. e. (B X. {{(/)}}) <-> (/) e. {{(/)}})
12	5, 11	orbi12i 255	. . . . . 6 |- ((<.x, (/)>. e. (A X. {(/)}) \/ <.x, (/)>. e. (B X. {{(/)}})) <-> (x e. A \/ (/) e. {{(/)}}))
13		elun 2225	. . . . . 6 |- (<.x, (/)>. e. ((A X. {(/)}) u. (B X. {{(/)}})) <-> (<.x, (/)>. e. (A X. {(/)}) \/ <.x, (/)>. e. (B X. {{(/)}})))
14	9	biorfi 741	. . . . . 6 |- (x e. A <-> (x e. A \/ (/) e. {{(/)}}))
15	12, 13, 14	3bitr4ri 182	. . . . 5 |- (x e. A <-> <.x, (/)>. e. ((A X. {(/)}) u. (B X. {{(/)}})))
16	2	opelxp 3297	. . . . . . . 8 |- (<.x, (/)>. e. (C X. {(/)}) <-> (x e. C /\ (/) e. {(/)}))
17	16, 4	mpbiran2 734	. . . . . . 7 |- (<.x, (/)>. e. (C X. {(/)}) <-> x e. C)
18	2	opelxp 3297	. . . . . . . 8 |- (<.x, (/)>. e. (D X. {{(/)}}) <-> (x e. D /\ (/) e. {{(/)}}))
19	9	bianfi 742	. . . . . . . 8 |- ((/) e. {{(/)}} <-> (x e. D /\ (/) e. {{(/)}}))
20	18, 19	bitr4i 174	. . . . . . 7 |- (<.x, (/)>. e. (D X. {{(/)}}) <-> (/) e. {{(/)}})
21	17, 20	orbi12i 255	. . . . . 6 |- ((<.x, (/)>. e. (C X. {(/)}) \/ <.x, (/)>. e. (D X. {{(/)}})) <-> (x e. C \/ (/) e. {{(/)}}))
22		elun 2225	. . . . . 6 |- (<.x, (/)>. e. ((C X. {(/)}) u. (D X. {{(/)}})) <-> (<.x, (/)>. e. (C X. {(/)}) \/ <.x, (/)>. e. (D X. {{(/)}})))
23	9	biorfi 741	. . . . . 6 |- (x e. C <-> (x e. C \/ (/) e. {{(/)}}))
24	21, 22, 23	3bitr4ri 182	. . . . 5 |- (x e. C <-> <.x, (/)>. e. ((C X. {(/)}) u. (D X. {{(/)}})))
25	1, 15, 24	3bitr4g 558	. . . 4 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (x e. A <-> x e. C))
26	25	eqrdv 1516	. . 3 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> A = C)
27		eleq2 1578	. . . . 5 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (<.x, {(/)}>. e. ((A X. {(/)}) u. (B X. {{(/)}})) <-> <.x, {(/)}>. e. ((C X. {(/)}) u. (D X. {{(/)}}))))
28		p0ex 2828	. . . . . . . . 9 |- {(/)} e. V
29	28	opelxp 3297	. . . . . . . 8 |- (<.x, {(/)}>. e. (A X. {(/)}) <-> (x e. A /\ {(/)} e. {(/)}))
30	28	elsnc 2492	. . . . . . . . . . 11 |- ({(/)} e. {(/)} <-> {(/)} = (/))
31		eqcom 1520	. . . . . . . . . . 11 |- ({(/)} = (/) <-> (/) = {(/)})
32	30, 31	bitri 171	. . . . . . . . . 10 |- ({(/)} e. {(/)} <-> (/) = {(/)})
33	7, 32	nemtbir 1687	. . . . . . . . 9 |- -. {(/)} e. {(/)}
34	33	bianfi 742	. . . . . . . 8 |- ({(/)} e. {(/)} <-> (x e. A /\ {(/)} e. {(/)}))
35	29, 34	bitr4i 174	. . . . . . 7 |- (<.x, {(/)}>. e. (A X. {(/)}) <-> {(/)} e. {(/)})
36	28	opelxp 3297	. . . . . . . 8 |- (<.x, {(/)}>. e. (B X. {{(/)}}) <-> (x e. B /\ {(/)} e. {{(/)}}))
37	28	snid 2496	. . . . . . . 8 |- {(/)} e. {{(/)}}
38	36, 37	mpbiran2 734	. . . . . . 7 |- (<.x, {(/)}>. e. (B X. {{(/)}}) <-> x e. B)
39	35, 38	orbi12i 255	. . . . . 6 |- ((<.x, {(/)}>. e. (A X. {(/)}) \/ <.x, {(/)}>. e. (B X. {{(/)}})) <-> ({(/)} e. {(/)} \/ x e. B))
40		elun 2225	. . . . . 6 |- (<.x, {(/)}>. e. ((A X. {(/)}) u. (B X. {{(/)}})) <-> (<.x, {(/)}>. e. (A X. {(/)}) \/ <.x, {(/)}>. e. (B X. {{(/)}})))
41		biorf 740	. . . . . . 7 |- (-. {(/)} e. {(/)} -> (x e. B <-> ({(/)} e. {(/)} \/ x e. B)))
42	33, 41	ax-mp 7	. . . . . 6 |- (x e. B <-> ({(/)} e. {(/)} \/ x e. B))
43	39, 40, 42	3bitr4ri 182	. . . . 5 |- (x e. B <-> <.x, {(/)}>. e. ((A X. {(/)}) u. (B X. {{(/)}})))
44	28	opelxp 3297	. . . . . . . 8 |- (<.x, {(/)}>. e. (C X. {(/)}) <-> (x e. C /\ {(/)} e. {(/)}))
45	33	bianfi 742	. . . . . . . 8 |- ({(/)} e. {(/)} <-> (x e. C /\ {(/)} e. {(/)}))
46	44, 45	bitr4i 174	. . . . . . 7 |- (<.x, {(/)}>. e. (C X. {(/)}) <-> {(/)} e. {(/)})
47	28	opelxp 3297	. . . . . . . 8 |- (<.x, {(/)}>. e. (D X. {{(/)}}) <-> (x e. D /\ {(/)} e. {{(/)}}))
48	47, 37	mpbiran2 734	. . . . . . 7 |- (<.x, {(/)}>. e. (D X. {{(/)}}) <-> x e. D)
49	46, 48	orbi12i 255	. . . . . 6 |- ((<.x, {(/)}>. e. (C X. {(/)}) \/ <.x, {(/)}>. e. (D X. {{(/)}})) <-> ({(/)} e. {(/)} \/ x e. D))
50		elun 2225	. . . . . 6 |- (<.x, {(/)}>. e. ((C X. {(/)}) u. (D X. {{(/)}})) <-> (<.x, {(/)}>. e. (C X. {(/)}) \/ <.x, {(/)}>. e. (D X. {{(/)}})))
51		biorf 740	. . . . . . 7 |- (-. {(/)} e. {(/)} -> (x e. D <-> ({(/)} e. {(/)} \/ x e. D)))
52	33, 51	ax-mp 7	. . . . . 6 |- (x e. D <-> ({(/)} e. {(/)} \/ x e. D))
53	49, 50, 52	3bitr4ri 182	. . . . 5 |- (x e. D <-> <.x, {(/)}>. e. ((C X. {(/)}) u. (D X. {{(/)}})))
54	27, 43, 53	3bitr4g 558	. . . 4 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (x e. B <-> x e. D))
55	54	eqrdv 1516	. . 3 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> B = D)
56	26, 55	jca 286	. 2 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (A = C /\ B = D))
57		uneq12 2231	. . 3 |- (((A X. {(/)}) = (C X. {(/)}) /\ (B X. {{(/)}}) = (D X. {{(/)}})) -> ((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})))
58		xpeq1 3281	. . 3 |- (A = C -> (A X. {(/)}) = (C X. {(/)}))
59		xpeq1 3281	. . 3 |- (B = D -> (B X. {{(/)}}) = (D X. {{(/)}}))
60	57, 58, 59	syl2an 456	. 2 |- ((A = C /\ B = D) -> ((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})))
61	56, 60	impbii 155	1 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) <-> (A = C /\ B = D))

Syntax hints:  -. wn 2   <-> wb 144   \/ wo 220   /\ wa 221   = wceq 992   e. wcel 994   u. cun 2097  (/)c0 2332  {csn 2467  <.cop 2469   X. cxp 3249

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-opab 2741  df-xp 3265

Copyright terms: Public domain