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 X. {(/)}) u. (B X. {{(/)}})) = ((C X. {(/)}) u. (D X. {{(/)}})) <-> (A = C /\ B = D))

Proof of Theorem opthprc

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