Theorem inf0 3457

Description: Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class "ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)" exists, is a subset of its union, and contains a given set y (and thus is non-empty). Thus it provides an example demonstrating that a set x exists with the necessary properties demanded by ax-inf 1079.

Hypothesis

Ref	Expression
inf0.1	⊢ ω ∈ V

Assertion

Ref	Expression
inf0	⊢ ∃x(y ∈ x ∧ ∀y(y ∈ x → ∃z(y ∈ z ∧ z ∈ x)))

Distinct variable group(s):   x,y,z

Proof of Theorem inf0

Step	Hyp	Ref	Expression
1		visset 1350	. . . . 5 ⊢ y ∈ V
2		frzer 2990	. . . . 5 ⊢ (y ∈ V → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘∅) = y)
3	1, 2	ax-mp 6	. . . 4 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘∅) = y
4		frfnom 2989	. . . . 5 ⊢ (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) Fn ω
5		peano1 2390	. . . . 5 ⊢ ∅ ∈ ω
6		fnfvrn 2889	. . . . 5 ⊢ (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘∅) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))
7	4, 5, 6	mp2an 520	. . . 4 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘∅) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)
8	3, 7	eqeltrr 1160	. . 3 ⊢ y ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)
9		fvelrn 2883	. . . . . 6 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) Fn ω → (u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ↔ ∃f ∈ ω ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u))
10	4, 9	ax-mp 6	. . . . 5 ⊢ (u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ↔ ∃f ∈ ω ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u)
11		eleq1 1149	. . . . . . . . . 10 ⊢ (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ↔ u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f)))
12		fvex 2838	. . . . . . . . . . . 12 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ V
13	12	sucid 2304	. . . . . . . . . . 11 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f)
14	12	sucex 2303	. . . . . . . . . . . . 13 ⊢ suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ V
15		ax-17 925	. . . . . . . . . . . . . 14 ⊢ (z ∈ y → ∀w z ∈ y)
16		ax-17 925	. . . . . . . . . . . . . 14 ⊢ (z ∈ f → ∀w z ∈ f)
17		hbopab1 2112	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ {⟨w, v⟩∣v = suc w} → ∀w z ∈ {⟨w, v⟩∣v = suc w})
18	17, 15	hbrdg 2974	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ rec({⟨w, v⟩∣v = suc w}, y) → ∀w z ∈ rec({⟨w, v⟩∣v = suc w}, y))
19		ax-17 925	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ ω → ∀w z ∈ ω)
20	18, 19	hbres 2577	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∀w z ∈ (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))
21	20, 16	hbfv 2837	. . . . . . . . . . . . . . 15 ⊢ (z ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) → ∀w z ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f))
22	21	hbsuc 2294	. . . . . . . . . . . . . 14 ⊢ (z ∈ suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) → ∀w z ∈ suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f))
23		cleqid 1102	. . . . . . . . . . . . . 14 ⊢ (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) = (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)
24		suceq 2288	. . . . . . . . . . . . . 14 ⊢ (w = ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) → suc w = suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f))
25	15, 16, 22, 23, 24	frsucopab 2992	. . . . . . . . . . . . 13 ⊢ ((f ∈ ω ∧ suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ V) → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) = suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f))
26	14, 25	mpan2 519	. . . . . . . . . . . 12 ⊢ (f ∈ ω → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) = suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f))
27	26	eleq2d 1156	. . . . . . . . . . 11 ⊢ (f ∈ ω → (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ↔ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ suc ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f)))
28	13, 27	mpbiri 169	. . . . . . . . . 10 ⊢ (f ∈ ω → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f))
29	11, 28	syl5bi 183	. . . . . . . . 9 ⊢ (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → (f ∈ ω → u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f)))
30		peano2b 2388	. . . . . . . . . . 11 ⊢ (f ∈ ω ↔ suc f ∈ ω)
31		fnfvrn 2889	. . . . . . . . . . . 12 ⊢ (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) Fn ω ∧ suc f ∈ ω) → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))
32	4, 31	mpan 518	. . . . . . . . . . 11 ⊢ (suc f ∈ ω → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))
33	30, 32	sylbi 174	. . . . . . . . . 10 ⊢ (f ∈ ω → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))
34	33	a1i 7	. . . . . . . . 9 ⊢ (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → (f ∈ ω → ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
35	29, 34	jcad 455	. . . . . . . 8 ⊢ (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → (f ∈ ω → (u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∧ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))
36	35	com12 13	. . . . . . 7 ⊢ (f ∈ ω → (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → (u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∧ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))
37		fvex 2838	. . . . . . . 8 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ V
38		eleq2 1150	. . . . . . . . 9 ⊢ (z = ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) → (u ∈ z ↔ u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f)))
39		eleq1 1149	. . . . . . . . 9 ⊢ (z = ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) → (z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ↔ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
40	38, 39	anbi12d 476	. . . . . . . 8 ⊢ (z = ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) → ((u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)) ↔ (u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∧ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))
41	37, 40	cla4ev 1401	. . . . . . 7 ⊢ ((u ∈ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∧ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘suc f) ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
42	36, 41	syl6 23	. . . . . 6 ⊢ (f ∈ ω → (((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))
43	42	r19.23aiv 1284	. . . . 5 ⊢ (∃f ∈ ω ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ‘f) = u → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
44	10, 43	sylbi 174	. . . 4 ⊢ (u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
45	44	ax-gen 677	. . 3 ⊢ ∀u(u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
46		fndm 2723	. . . . . . 7 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) Fn ω → dom (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) = ω)
47	4, 46	ax-mp 6	. . . . . 6 ⊢ dom (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) = ω
48		inf0.1	. . . . . 6 ⊢ ω ∈ V
49	47, 48	eqeltr 1159	. . . . 5 ⊢ dom (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ∈ V
50		fnfun 2721	. . . . . 6 ⊢ ((rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) Fn ω → Fun (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))
51	4, 50	ax-mp 6	. . . . 5 ⊢ Fun (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)
52		funrnex 2743	. . . . 5 ⊢ (dom (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ∈ V → (Fun (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ∈ V))
53	49, 51, 52	mp2 43	. . . 4 ⊢ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ∈ V
54		eleq2 1150	. . . . 5 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → (y ∈ x ↔ y ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
55		eleq2 1150	. . . . . . 7 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → (u ∈ x ↔ u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
56		eleq2 1150	. . . . . . . . 9 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → (z ∈ x ↔ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))
57	56	anbi2d 468	. . . . . . . 8 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ((u ∈ z ∧ z ∈ x) ↔ (u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))
58	57	biexdv 936	. . . . . . 7 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → (∃z(u ∈ z ∧ z ∈ x) ↔ ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))
59	55, 58	imbi12d 474	. . . . . 6 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ((u ∈ x → ∃z(u ∈ z ∧ z ∈ x)) ↔ (u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))))
60	59	bialdv 935	. . . . 5 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → (∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x)) ↔ ∀u(u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))))
61	54, 60	anbi12d 476	. . . 4 ⊢ (x = ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ((y ∈ x ∧ ∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x))) ↔ (y ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ∧ ∀u(u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω))))))
62	53, 61	cla4ev 1401	. . 3 ⊢ ((y ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) ∧ ∀u(u ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω) → ∃z(u ∈ z ∧ z ∈ ran (rec({⟨w, v⟩∣v = suc w}, y) ↾ ω)))) → ∃x(y ∈ x ∧ ∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x))))
63	8, 45, 62	mp2an 520	. 2 ⊢ ∃x(y ∈ x ∧ ∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x)))
64		eleq1 1149	. . . . . 6 ⊢ (y = u → (y ∈ x ↔ u ∈ x))
65		eleq1 1149	. . . . . . . 8 ⊢ (y = u → (y ∈ z ↔ u ∈ z))
66	65	anbi1d 469	. . . . . . 7 ⊢ (y = u → ((y ∈ z ∧ z ∈ x) ↔ (u ∈ z ∧ z ∈ x)))
67	66	biexdv 936	. . . . . 6 ⊢ (y = u → (∃z(y ∈ z ∧ z ∈ x) ↔ ∃z(u ∈ z ∧ z ∈ x)))
68	64, 67	imbi12d 474	. . . . 5 ⊢ (y = u → ((y ∈ x → ∃z(y ∈ z ∧ z ∈ x)) ↔ (u ∈ x → ∃z(u ∈ z ∧ z ∈ x))))
69	68	cbvalv 972	. . . 4 ⊢ (∀y(y ∈ x → ∃z(y ∈ z ∧ z ∈ x)) ↔ ∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x)))
70	69	anbi2i 367	. . 3 ⊢ ((y ∈ x ∧ ∀y(y ∈ x → ∃z(y ∈ z ∧ z ∈ x))) ↔ (y ∈ x ∧ ∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x))))
71	70	biex 733	. 2 ⊢ (∃x(y ∈ x ∧ ∀y(y ∈ x → ∃z(y ∈ z ∧ z ∈ x))) ↔ ∃x(y ∈ x ∧ ∀u(u ∈ x → ∃z(u ∈ z ∧ z ∈ x))))
72	63, 71	mpbir 165	1 ⊢ ∃x(y ∈ x ∧ ∀y(y ∈ x → ∃z(y ∈ z ∧ z ∈ x)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348  ∅c0 1707  {copab 2055  suc csuc 2201  ωcom 2372  dom cdm 2410  ran crn 2411   ↾ cres 2412  Fun wfun 2416   Fn wfn 2417   ‘cfv 2422  reccrdg 2969

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438  df-rdg 2970

metamath.org