Theorem zfpair 2773

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 2774. Instead, use zfpair2 2776 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 2419	. 2 ⊢ {x, y} = {w∣(w = x ⋁ w = y)}
2		19.43 1087	. . . . 5 ⊢ (∃z((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ (∃z(z = ∅ ⋀ w = x) ⋁ ∃z(z = {∅} ⋀ w = y)))
3		prlem2 770	. . . . . 6 ⊢ (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
4	3	exbii 1050	. . . . 5 ⊢ (∃z((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
5		19.41v 1304	. . . . . . 7 ⊢ (∃z(z = ∅ ⋀ w = x) ↔ (∃z z = ∅ ⋀ w = x))
6		0ex 2707	. . . . . . . 8 ⊢ ∅ ∈ V
7	6	isseti 1812	. . . . . . 7 ⊢ ∃z z = ∅
8	5, 7	mpbiran 727	. . . . . 6 ⊢ (∃z(z = ∅ ⋀ w = x) ↔ w = x)
9		19.41v 1304	. . . . . . 7 ⊢ (∃z(z = {∅} ⋀ w = y) ↔ (∃z z = {∅} ⋀ w = y))
10		p0ex 2766	. . . . . . . 8 ⊢ {∅} ∈ V
11	10	isseti 1812	. . . . . . 7 ⊢ ∃z z = {∅}
12	9, 11	mpbiran 727	. . . . . 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 1573	. . 3 ⊢ {w∣(w = x ⋁ w = y)} = {w∣∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)))}
16		dfpr2 2419	. . . . 5 ⊢ {∅, {∅}} = {z∣(z = ∅ ⋁ z = {∅})}
17		pp0ex 2767	. . . . 5 ⊢ {∅, {∅}} ∈ V
18	16, 17	eqeltrr 1543	. . . 4 ⊢ {z∣(z = ∅ ⋁ z = {∅})} ∈ V
19		equequ2 1134	. . . . . . . 8 ⊢ (v = x → (w = v ↔ w = x))
20		0inp0 2734	. . . . . . . 8 ⊢ (z = ∅ → ¬ z = {∅})
21	19, 20	prlem1 769	. . . . . . 7 ⊢ (v = x → (z = ∅ → (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
22	21	19.21adv 1287	. . . . . 6 ⊢ (v = x → (z = ∅ → ∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
23	22	a4imev 1272	. . . . 5 ⊢ (z = ∅ → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
24		equequ2 1134	. . . . . . . . 9 ⊢ (v = y → (w = v ↔ w = y))
25	20	con2i 97	. . . . . . . . 9 ⊢ (z = {∅} → ¬ z = ∅)
26	24, 25	prlem1 769	. . . . . . . 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 1287	. . . . . 6 ⊢ (v = y → (z = {∅} → ∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
30	29	a4imev 1272	. . . . 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 2697	. . 3 ⊢ {w∣∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)))} ∈ V
33	15, 32	eqeltr 1542	. 2 ⊢ {w∣(w = x ⋁ w = y)} ∈ V
34	1, 33	eqeltr 1542	1 ⊢ {x, y} ∈ V

Syntax hints:   → wi 3   ⋁ wo 222   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979  {cab 1462  Vcvv 1808  ∅c0 2277  {csn 2406  {cpr 2407

This theorem is referenced by:  axpr 2774

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410

Copyright terms: Public domain