Theorem zfpair 2767

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 axpr 2768. Instead, use zfpair2 2770 below so that the uses of the Axiom of Pairing can be more easily identified.

Assertion

Ref	Expression
zfpair	⊢ {x, y} ∈ V

Proof of Theorem zfpair

Step	Hyp	Ref	Expression
1		dfpr2 2412	. 2 ⊢ {x, y} = {w∣(w = x ⋁ w = y)}
2		19.43 1084	. . . . 5 ⊢ (∃z((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ (∃z(z = ∅ ⋀ w = x) ⋁ ∃z(z = {∅} ⋀ w = y)))
3		prlem2 769	. . . . . 6 ⊢ (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
4	3	exbii 1047	. . . . 5 ⊢ (∃z((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
5		19.41v 1300	. . . . . . 7 ⊢ (∃z(z = ∅ ⋀ w = x) ↔ (∃z z = ∅ ⋀ w = x))
6		0ex 2701	. . . . . . . 8 ⊢ ∅ ∈ V
7	6	isseti 1806	. . . . . . 7 ⊢ ∃z z = ∅
8	5, 7	mpbiran 726	. . . . . 6 ⊢ (∃z(z = ∅ ⋀ w = x) ↔ w = x)
9		19.41v 1300	. . . . . . 7 ⊢ (∃z(z = {∅} ⋀ w = y) ↔ (∃z z = {∅} ⋀ w = y))
10		p0ex 2760	. . . . . . . 8 ⊢ {∅} ∈ V
11	10	isseti 1806	. . . . . . 7 ⊢ ∃z z = {∅}
12	9, 11	mpbiran 726	. . . . . 6 ⊢ (∃z(z = {∅} ⋀ w = y) ↔ w = y)
13	8, 12	orbi12i 257	. . . . 5 ⊢ ((∃z(z = ∅ ⋀ w = x) ⋁ ∃z(z = {∅} ⋀ w = y)) ↔ (w = x ⋁ w = y))
14	2, 4, 13	3bitr3r 182	. . . 4 ⊢ ((w = x ⋁ w = y) ↔ ∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
15	14	abbii 1567	. . 3 ⊢ {w∣(w = x ⋁ w = y)} = {w∣∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)))}
16		dfpr2 2412	. . . . 5 ⊢ {∅, {∅}} = {z∣(z = ∅ ⋁ z = {∅})}
17		pp0ex 2761	. . . . 5 ⊢ {∅, {∅}} ∈ V
18	16, 17	eqeltrr 1537	. . . 4 ⊢ {z∣(z = ∅ ⋁ z = {∅})} ∈ V
19		equequ2 1131	. . . . . . . 8 ⊢ (v = x → (w = v ↔ w = x))
20		0inp0 2728	. . . . . . . 8 ⊢ (z = ∅ → ¬ z = {∅})
21	19, 20	prlem1 768	. . . . . . 7 ⊢ (v = x → (z = ∅ → (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
22	21	19.21adv 1283	. . . . . 6 ⊢ (v = x → (z = ∅ → ∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
23	22	a4imev 1268	. . . . 5 ⊢ (z = ∅ → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
24		equequ2 1131	. . . . . . . . 9 ⊢ (v = y → (w = v ↔ w = y))
25	20	con2i 97	. . . . . . . . 9 ⊢ (z = {∅} → ¬ z = ∅)
26	24, 25	prlem1 768	. . . . . . . 8 ⊢ (v = y → (z = {∅} → (((z = {∅} ⋀ w = y) ⋁ (z = ∅ ⋀ w = x)) → w = v)))
27		orcom 246	. . . . . . . 8 ⊢ (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ((z = {∅} ⋀ w = y) ⋁ (z = ∅ ⋀ w = x)))
28	26, 27	syl7ib 216	. . . . . . 7 ⊢ (v = y → (z = {∅} → (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
29	28	19.21adv 1283	. . . . . 6 ⊢ (v = y → (z = {∅} → ∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
30	29	a4imev 1268	. . . . 5 ⊢ (z = {∅} → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
31	23, 30	jaoi 341	. . . 4 ⊢ ((z = ∅ ⋁ z = {∅}) → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
32	18, 31	zfrep4 2691	. . 3 ⊢ {w∣∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)))} ∈ V
33	15, 32	eqeltr 1536	. 2 ⊢ {w∣(w = x ⋁ w = y)} ∈ V
34	1, 33	eqeltr 1536	1 ⊢ {x, y} ∈ V

Syntax hints:   → wi 3   ⋁ wo 222   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∃wex 977  {cab 1456  Vcvv 1802  ∅c0 2270  {csn 2399  {cpr 2400

This theorem is referenced by:  axpr 2768

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403

Copyright terms: Public domain