Theorem opthprc 3227

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 1538	. . . . 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 2716	. . . . . . . . 9 |- (/) e. V
3	2	opelxp 3220	. . . . . . . 8 |- (<.x, (/)>. e. (A X. {(/)}) <-> (x e. A /\ (/) e. {(/)}))
4	2	snid 2439	. . . . . . . 8 |- (/) e. {(/)}
5	3, 4	mpbiran2 731	. . . . . . 7 |- (<.x, (/)>. e. (A X. {(/)}) <-> x e. A)
6	2	opelxp 3220	. . . . . . . 8 |- (<.x, (/)>. e. (B X. {{(/)}}) <-> (x e. B /\ (/) e. {{(/)}}))
7		0nep0 2742	. . . . . . . . . 10 |- (/) =/= {(/)}
8	2	elsnc 2435	. . . . . . . . . 10 |- ((/) e. {{(/)}} <-> (/) = {(/)})
9	7, 8	nemtbir 1644	. . . . . . . . 9 |- -. (/) e. {{(/)}}
10	9	bianfi 739	. . . . . . . 8 |- ((/) e. {{(/)}} <-> (x e. B /\ (/) e. {{(/)}}))
11	6, 10	bitr4 176	. . . . . . 7 |- (<.x, (/)>. e. (B X. {{(/)}}) <-> (/) e. {{(/)}})
12	5, 11	orbi12i 257	. . . . . 6 |- ((<.x, (/)>. e. (A X. {(/)}) \/ <.x, (/)>. e. (B X. {{(/)}})) <-> (x e. A \/ (/) e. {{(/)}}))
13		elun 2176	. . . . . 6 |- (<.x, (/)>. e. ((A X. {(/)}) u. (B X. {{(/)}})) <-> (<.x, (/)>. e. (A X. {(/)}) \/ <.x, (/)>. e. (B X. {{(/)}})))
14	9	biorfi 738	. . . . . 6 |- (x e. A <-> (x e. A \/ (/) e. {{(/)}}))
15	12, 13, 14	3bitr4r 184	. . . . 5 |- (x e. A <-> <.x, (/)>. e. ((A X. {(/)}) u. (B X. {{(/)}})))
16	2	opelxp 3220	. . . . . . . 8 |- (<.x, (/)>. e. (C X. {(/)}) <-> (x e. C /\ (/) e. {(/)}))
17	16, 4	mpbiran2 731	. . . . . . 7 |- (<.x, (/)>. e. (C X. {(/)}) <-> x e. C)
18	2	opelxp 3220	. . . . . . . 8 |- (<.x, (/)>. e. (D X. {{(/)}}) <-> (x e. D /\ (/) e. {{(/)}}))
19	9	bianfi 739	. . . . . . . 8 |- ((/) e. {{(/)}} <-> (x e. D /\ (/) e. {{(/)}}))
20	18, 19	bitr4 176	. . . . . . 7 |- (<.x, (/)>. e. (D X. {{(/)}}) <-> (/) e. {{(/)}})
21	17, 20	orbi12i 257	. . . . . 6 |- ((<.x, (/)>. e. (C X. {(/)}) \/ <.x, (/)>. e. (D X. {{(/)}})) <-> (x e. C \/ (/) e. {{(/)}}))
22		elun 2176	. . . . . 6 |- (<.x, (/)>. e. ((C X. {(/)}) u. (D X. {{(/)}})) <-> (<.x, (/)>. e. (C X. {(/)}) \/ <.x, (/)>. e. (D X. {{(/)}})))
23	9	biorfi 738	. . . . . 6 |- (x e. C <-> (x e. C \/ (/) e. {{(/)}}))
24	21, 22, 23	3bitr4r 184	. . . . 5 |- (x e. C <-> <.x, (/)>. e. ((C X. {(/)}) u. (D X. {{(/)}})))
25	1, 15, 24	3bitr4g 557	. . . 4 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (x e. A <-> x e. C))
26	25	eqrdv 1476	. . 3 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> A = C)
27		eleq2 1538	. . . . 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 2776	. . . . . . . . 9 |- {(/)} e. V
29	28	opelxp 3220	. . . . . . . 8 |- (<.x, {(/)}>. e. (A X. {(/)}) <-> (x e. A /\ {(/)} e. {(/)}))
30	28	elsnc 2435	. . . . . . . . . . 11 |- ({(/)} e. {(/)} <-> {(/)} = (/))
31		eqcom 1480	. . . . . . . . . . 11 |- ({(/)} = (/) <-> (/) = {(/)})
32	30, 31	bitr 173	. . . . . . . . . 10 |- ({(/)} e. {(/)} <-> (/) = {(/)})
33	7, 32	nemtbir 1644	. . . . . . . . 9 |- -. {(/)} e. {(/)}
34	33	bianfi 739	. . . . . . . 8 |- ({(/)} e. {(/)} <-> (x e. A /\ {(/)} e. {(/)}))
35	29, 34	bitr4 176	. . . . . . 7 |- (<.x, {(/)}>. e. (A X. {(/)}) <-> {(/)} e. {(/)})
36	28	opelxp 3220	. . . . . . . 8 |- (<.x, {(/)}>. e. (B X. {{(/)}}) <-> (x e. B /\ {(/)} e. {{(/)}}))
37	28	snid 2439	. . . . . . . 8 |- {(/)} e. {{(/)}}
38	36, 37	mpbiran2 731	. . . . . . 7 |- (<.x, {(/)}>. e. (B X. {{(/)}}) <-> x e. B)
39	35, 38	orbi12i 257	. . . . . 6 |- ((<.x, {(/)}>. e. (A X. {(/)}) \/ <.x, {(/)}>. e. (B X. {{(/)}})) <-> ({(/)} e. {(/)} \/ x e. B))
40		elun 2176	. . . . . 6 |- (<.x, {(/)}>. e. ((A X. {(/)}) u. (B X. {{(/)}})) <-> (<.x, {(/)}>. e. (A X. {(/)}) \/ <.x, {(/)}>. e. (B X. {{(/)}})))
41		biorf 737	. . . . . . 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	3bitr4r 184	. . . . 5 |- (x e. B <-> <.x, {(/)}>. e. ((A X. {(/)}) u. (B X. {{(/)}})))
44	28	opelxp 3220	. . . . . . . 8 |- (<.x, {(/)}>. e. (C X. {(/)}) <-> (x e. C /\ {(/)} e. {(/)}))
45	33	bianfi 739	. . . . . . . 8 |- ({(/)} e. {(/)} <-> (x e. C /\ {(/)} e. {(/)}))
46	44, 45	bitr4 176	. . . . . . 7 |- (<.x, {(/)}>. e. (C X. {(/)}) <-> {(/)} e. {(/)})
47	28	opelxp 3220	. . . . . . . 8 |- (<.x, {(/)}>. e. (D X. {{(/)}}) <-> (x e. D /\ {(/)} e. {{(/)}}))
48	47, 37	mpbiran2 731	. . . . . . 7 |- (<.x, {(/)}>. e. (D X. {{(/)}}) <-> x e. D)
49	46, 48	orbi12i 257	. . . . . 6 |- ((<.x, {(/)}>. e. (C X. {(/)}) \/ <.x, {(/)}>. e. (D X. {{(/)}})) <-> ({(/)} e. {(/)} \/ x e. D))
50		elun 2176	. . . . . 6 |- (<.x, {(/)}>. e. ((C X. {(/)}) u. (D X. {{(/)}})) <-> (<.x, {(/)}>. e. (C X. {(/)}) \/ <.x, {(/)}>. e. (D X. {{(/)}})))
51		biorf 737	. . . . . . 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	3bitr4r 184	. . . . 5 |- (x e. D <-> <.x, {(/)}>. e. ((C X. {(/)}) u. (D X. {{(/)}})))
54	27, 43, 53	3bitr4g 557	. . . 4 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (x e. B <-> x e. D))
55	54	eqrdv 1476	. . 3 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> B = D)
56	26, 55	jca 288	. 2 |- (((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) -> (A = C /\ B = D))
57		uneq12 2182	. . 3 |- (((A X. {(/)}) = (C X. {(/)}) /\ (B X. {{(/)}}) = (D X. {{(/)}})) -> ((A X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {