Theorem zfpair

Description: The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of TakeutiZaring p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms.

This theorem should not be referenced by any proof other than axprALT . Instead, use zfpair2 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	zfpair	$$⊢\left\{x,y\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfpr2	$$⊢\left\{x,y\right\}=\left\{w|\left(w=x\vee w=y\right)\right\}$$
2		19.43	$$⊢\exists z\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\leftrightarrow \left(\exists z\left(z=\varnothing \wedge w=x\right)\vee \exists z\left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)$$
3		prlem2	$$⊢\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\leftrightarrow \left(\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\wedge \left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\right)$$
4	3	exbii	$$⊢\exists z\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\leftrightarrow \exists z\left(\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\wedge \left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\right)$$
5		0ex	$$⊢\varnothing \in \mathrm{V}$$
6	5	isseti	$$⊢\exists zz=\varnothing$$
7		19.41v	$$⊢\exists z\left(z=\varnothing \wedge w=x\right)\leftrightarrow \left(\exists zz=\varnothing \wedge w=x\right)$$
8	6 7	mpbiran	$$⊢\exists z\left(z=\varnothing \wedge w=x\right)\leftrightarrow w=x$$
9		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
10	9	isseti	$$⊢\exists zz=\left\{\varnothing \right\}$$
11		19.41v	$$⊢\exists z\left(z=\left\{\varnothing \right\}\wedge w=y\right)\leftrightarrow \left(\exists zz=\left\{\varnothing \right\}\wedge w=y\right)$$
12	10 11	mpbiran	$$⊢\exists z\left(z=\left\{\varnothing \right\}\wedge w=y\right)\leftrightarrow w=y$$
13	8 12	orbi12i	$$⊢\left(\exists z\left(z=\varnothing \wedge w=x\right)\vee \exists z\left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\leftrightarrow \left(w=x\vee w=y\right)$$
14	2 4 13	3bitr3ri	$$⊢\left(w=x\vee w=y\right)\leftrightarrow \exists z\left(\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\wedge \left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\right)$$
15	14	abbii	$$⊢\left\{w|\left(w=x\vee w=y\right)\right\}=\left\{w|\exists z\left(\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\wedge \left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\right)\right\}$$
16		dfpr2	$$⊢\left\{\varnothing ,\left\{\varnothing \right\}\right\}=\left\{z|\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\right\}$$
17		pp0ex	$$⊢\left\{\varnothing ,\left\{\varnothing \right\}\right\}\in \mathrm{V}$$
18	16 17	eqeltrri	$$⊢\left\{z|\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\right\}\in \mathrm{V}$$
19		equequ2	$$⊢v=x\to \left(w=v\leftrightarrow w=x\right)$$
20		0inp0	$$⊢z=\varnothing \to \neg z=\left\{\varnothing \right\}$$
21	19 20	prlem1	$$⊢v=x\to \left(z=\varnothing \to \left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)\right)$$
22	21	alrimdv	$$⊢v=x\to \left(z=\varnothing \to \forall w\left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)\right)$$
23	22	spimevw	$$⊢z=\varnothing \to \exists v\forall w\left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)$$
24		orcom	$$⊢\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\leftrightarrow \left(\left(z=\left\{\varnothing \right\}\wedge w=y\right)\vee \left(z=\varnothing \wedge w=x\right)\right)$$
25		equequ2	$$⊢v=y\to \left(w=v\leftrightarrow w=y\right)$$
26	20	con2i	$$⊢z=\left\{\varnothing \right\}\to \neg z=\varnothing$$
27	25 26	prlem1	$$⊢v=y\to \left(z=\left\{\varnothing \right\}\to \left(\left(\left(z=\left\{\varnothing \right\}\wedge w=y\right)\vee \left(z=\varnothing \wedge w=x\right)\right)\to w=v\right)\right)$$
28	24 27	syl7bi	$$⊢v=y\to \left(z=\left\{\varnothing \right\}\to \left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)\right)$$
29	28	alrimdv	$$⊢v=y\to \left(z=\left\{\varnothing \right\}\to \forall w\left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)\right)$$
30	29	spimevw	$$⊢z=\left\{\varnothing \right\}\to \exists v\forall w\left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)$$
31	23 30	jaoi	$$⊢\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\to \exists v\forall w\left(\left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\to w=v\right)$$
32	18 31	zfrep4	$$⊢\left\{w|\exists z\left(\left(z=\varnothing \vee z=\left\{\varnothing \right\}\right)\wedge \left(\left(z=\varnothing \wedge w=x\right)\vee \left(z=\left\{\varnothing \right\}\wedge w=y\right)\right)\right)\right\}\in \mathrm{V}$$
33	15 32	eqeltri	$$⊢\left\{w|\left(w=x\vee w=y\right)\right\}\in \mathrm{V}$$
34	1 33	eqeltri	$$⊢\left\{x,y\right\}\in \mathrm{V}$$