Theorem axinfnd 4941

Description: A version of the Axiom of Infinity with no distinct variable conditions.

Assertion

Ref	Expression
axinfnd	⊢ ∃x(y ∈ z → (y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))

Proof of Theorem axinfnd

Step	Hyp	Ref	Expression
1		axinfndlem1 4940	. . . . . . 7 ⊢ (∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))))
2	1	ax-gen 962	. . . . . 6 ⊢ ∀w(∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))))
3		hbnae 1146	. . . . . . . 8 ⊢ (¬ ∀y y = x → ∀y ¬ ∀y y = x)
4		hbnae 1146	. . . . . . . 8 ⊢ (¬ ∀y y = z → ∀y ¬ ∀y y = z)
5	3, 4	hban 1008	. . . . . . 7 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ∀y(¬ ∀y y = x ⋀ ¬ ∀y y = z))
6		hbnae 1146	. . . . . . . . . 10 ⊢ (¬ ∀y y = z → ∀x ¬ ∀y y = z)
7		dveel2 1356	. . . . . . . . . 10 ⊢ (¬ ∀y y = z → (w ∈ z → ∀y w ∈ z))
8	6, 7	hbald 1112	. . . . . . . . 9 ⊢ (¬ ∀y y = z → (∀x w ∈ z → ∀y∀x w ∈ z))
9	8	adantl 388	. . . . . . . 8 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∀x w ∈ z → ∀y∀x w ∈ z))
10		hbnae 1146	. . . . . . . . . 10 ⊢ (¬ ∀y y = x → ∀x ¬ ∀y y = x)
11	10, 6	hban 1008	. . . . . . . . 9 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ∀x(¬ ∀y y = x ⋀ ¬ ∀y y = z))
12		dveel2 1356	. . . . . . . . . . 11 ⊢ (¬ ∀y y = x → (w ∈ x → ∀y w ∈ x))
13	12	adantr 389	. . . . . . . . . 10 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (w ∈ x → ∀y w ∈ x))
14		ax-17 970	. . . . . . . . . . 11 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ∀w(¬ ∀y y = x ⋀ ¬ ∀y y = z))
15		hbnae 1146	. . . . . . . . . . . . . 14 ⊢ (¬ ∀y y = x → ∀z ¬ ∀y y = x)
16		hbnae 1146	. . . . . . . . . . . . . 14 ⊢ (¬ ∀y y = z → ∀z ¬ ∀y y = z)
17	15, 16	hban 1008	. . . . . . . . . . . . 13 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ∀z(¬ ∀y y = x ⋀ ¬ ∀y y = z))
18	7	adantl 388	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (w ∈ z → ∀y w ∈ z))
19		ax-15 1359	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀y y = z → (¬ ∀y y = x → (z ∈ x → ∀y z ∈ x)))
20	19	impcom 351	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (z ∈ x → ∀y z ∈ x))
21	18, 20	hband 1110	. . . . . . . . . . . . 13 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ((w ∈ z ⋀ z ∈ x) → ∀y(w ∈ z ⋀ z ∈ x)))
22	17, 21	hbexd 1113	. . . . . . . . . . . 12 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∃z(w ∈ z ⋀ z ∈ x) → ∀y∃z(w ∈ z ⋀ z ∈ x)))
23	5, 13, 22	hbimd 1109	. . . . . . . . . . 11 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ((w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)) → ∀y(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))))
24	14, 23	hbald 1112	. . . . . . . . . 10 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)) → ∀y∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))))
25	13, 24	hband 1110	. . . . . . . . 9 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ((w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))) → ∀y(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))))
26	11, 25	hbexd 1113	. . . . . . . 8 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))) → ∀y∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))))
27	5, 9, 26	hbimd 1109	. . . . . . 7 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ((∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))) → ∀y(∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))))))
28		nd5 4925	. . . . . . . . . . 11 ⊢ (¬ ∀y y = x → (w = y → ∀x w = y))
29	28	adantr 389	. . . . . . . . . 10 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (w = y → ∀x w = y))
30	29	imdistani 443	. . . . . . . . 9 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ w = y) → ((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y))
31		hba1 1002	. . . . . . . . . . . 12 ⊢ (∀x w = y → ∀x∀x w = y)
32		elequ1 1135	. . . . . . . . . . . . 13 ⊢ (w = y → (w ∈ z ↔ y ∈ z))
33	32	a4s 983	. . . . . . . . . . . 12 ⊢ (∀x w = y → (w ∈ z ↔ y ∈ z))
34	31, 33	albid 1103	. . . . . . . . . . 11 ⊢ (∀x w = y → (∀x w ∈ z ↔ ∀x y ∈ z))
35	34	adantl 388	. . . . . . . . . 10 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y) → (∀x w ∈ z ↔ ∀x y ∈ z))
36	11, 31	hban 1008	. . . . . . . . . . 11 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y) → ∀x((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y))
37		elequ1 1135	. . . . . . . . . . . . 13 ⊢ (w = y → (w ∈ x ↔ y ∈ x))
38	37	a4s 983	. . . . . . . . . . . 12 ⊢ (∀x w = y → (w ∈ x ↔ y ∈ x))
39	37	adantl 388	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∀y y = z ⋀ w = y) → (w ∈ x ↔ y ∈ x))
40		nd5 4925	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∀y y = z → (w = y → ∀z w = y))
41	40	imdistani 443	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ ∀y y = z ⋀ w = y) → (¬ ∀y y = z ⋀ ∀z w = y))
42		hba1 1002	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀z w = y → ∀z∀z w = y)
43	32	anbi1d 616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (w = y → ((w ∈ z ⋀ z ∈ x) ↔ (y ∈ z ⋀ z ∈ x)))
44	43	a4s 983	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀z w = y → ((w ∈ z ⋀ z ∈ x) ↔ (y ∈ z ⋀ z ∈ x)))
45	42, 44	exbid 1104	. . . . . . . . . . . . . . . . . 18 ⊢ (∀z w = y → (∃z(w ∈ z ⋀ z ∈ x) ↔ ∃z(y ∈ z ⋀ z ∈ x)))
46	45	adantl 388	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ ∀y y = z ⋀ ∀z w = y) → (∃z(w ∈ z ⋀ z ∈ x) ↔ ∃z(y ∈ z ⋀ z ∈ x)))
47	41, 46	syl 10	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∀y y = z ⋀ w = y) → (∃z(w ∈ z ⋀ z ∈ x) ↔ ∃z(y ∈ z ⋀ z ∈ x)))
48	39, 47	imbi12d 625	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀y y = z ⋀ w = y) → ((w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)) ↔ (y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))
49	48	adantll 392	. . . . . . . . . . . . . 14 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ w = y) → ((w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)) ↔ (y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))
50	49	ex 373	. . . . . . . . . . . . 13 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (w = y → ((w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)) ↔ (y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
51	5, 23, 50	cbvald 1319	. . . . . . . . . . . 12 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)) ↔ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))
52	38, 51	bi2anan9r 632	. . . . . . . . . . 11 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y) → ((w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))) ↔ (y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
53	36, 52	exbid 1104	. . . . . . . . . 10 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y) → (∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x))) ↔ ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
54	35, 53	imbi12d 625	. . . . . . . . 9 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ ∀x w = y) → ((∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))) ↔ (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))))
55	30, 54	syl 10	. . . . . . . 8 ⊢ (((¬ ∀y y = x ⋀ ¬ ∀y y = z) ⋀ w = y) → ((∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))) ↔ (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))))
56	55	ex 373	. . . . . . 7 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (w = y → ((∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))) ↔ (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))))
57	5, 27, 56	cbvald 1319	. . . . . 6 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∀w(∀x w ∈ z → ∃x(w ∈ x ⋀ ∀w(w ∈ x → ∃z(w ∈ z ⋀ z ∈ x)))) ↔ ∀y(∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))))
58	2, 57	mpbii 193	. . . . 5 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → ∀y(∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
59	58	19.21bi 1059	. . . 4 ⊢ ((¬ ∀y y = x ⋀ ¬ ∀y y = z) → (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
60	59	ex 373	. . 3 ⊢ (¬ ∀y y = x → (¬ ∀y y = z → (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))))
61		nd1 4921	. . . . 5 ⊢ (∀x x = y → ¬ ∀x y ∈ z)
62	61	alequcoms 1142	. . . 4 ⊢ (∀y y = x → ¬ ∀x y ∈ z)
63	62	pm2.21d 78	. . 3 ⊢ (∀y y = x → (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
64		nd3 4923	. . . 4 ⊢ (∀y y = z → ¬ ∀x y ∈ z)
65	64	pm2.21d 78	. . 3 ⊢ (∀y y = z → (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))))
66	60, 63, 65	pm2.61ii 130	. 2 ⊢ (∀x y ∈ z → ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))
67	66	19.35ri 1076	1 ⊢ ∃x(y ∈ z → (y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x))))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979

This theorem is referenced by:  zfcndinf 4953

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-15 1359  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-reg 4576  ax-inf 4605

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-ral 1647  df-rex 1648  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