Theorem axinfndlem1 10624

Description: Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.)

Assertion

Ref	Expression
axinfndlem1	⊢ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))

Distinct variable group:   𝑦,𝑧

Proof of Theorem axinfndlem1

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfinf 9658	. . . . 5 ⊢ ∃𝑤(𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
2		nfnae 2439	. . . . . . 7 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
3		nfnae 2439	. . . . . . 7 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑧
4	2, 3	nfan 1899	. . . . . 6 ⊢ Ⅎ𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
5		nfcvf 2926	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
6	5	adantr 480	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦)
7		nfcvd 2900	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤)
8	6, 7	nfeld 2911	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑤)
9		nfnae 2439	. . . . . . . . 9 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
10		nfnae 2439	. . . . . . . . 9 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑧
11	9, 10	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
12		nfnae 2439	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
13		nfnae 2439	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑧
14	12, 13	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
15		nfcvf 2926	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧)
16	15	adantl 481	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧)
17	6, 16	nfeld 2911	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑧)
18	16, 7	nfeld 2911	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 ∈ 𝑤)
19	17, 18	nfand 1897	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))
20	14, 19	nfexd 2330	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))
21	8, 20	nfimd 1894	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
22	11, 21	nfald 2329	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
23	8, 22	nfand 1897	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))))
24		simpr 484	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → 𝑤 = 𝑥)
25	24	eleq2d 2821	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥))
26		nfcvd 2900	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑤)
27		nfcvf2 2927	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
28	27	adantr 480	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑥)
29	26, 28	nfeqd 2910	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥)
30	11, 29	nfan1 2201	. . . . . . . . 9 ⊢ Ⅎ𝑦((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
31		nfcvd 2900	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑤)
32		nfcvf2 2927	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥)
33	32	adantl 481	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑥)
34	31, 33	nfeqd 2910	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥)
35	14, 34	nfan1 2201	. . . . . . . . . . 11 ⊢ Ⅎ𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥)
36		elequ2 2124	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥))
37	36	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
38	37	adantl 481	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
39	35, 38	exbid 2224	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
40	25, 39	imbi12d 344	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) ↔ (𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))
41	30, 40	albid 2223	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))
42	25, 41	anbi12d 632	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))
43	42	ex 412	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))))
44	4, 23, 43	cbvexd 2413	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))
45	1, 44	mpbii 233	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))
46	45	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))
47	46	ex 412	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))))
48		nd1 10606	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑦 ∈ 𝑧)
49	48	pm2.21d 121	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))
50		nd2 10607	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑦 ∈ 𝑧)
51	50	pm2.21d 121	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))
52	47, 49, 51	pm2.61ii 183	1 ⊢ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2377  ax-ext 2708  ax-sep 5271  ax-pr 5407  ax-reg 9611  ax-inf 9657

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-v 3466  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  axinfnd  10625