Theorem inf0 4586

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

Hypothesis

Ref	Expression
inf0.1	|- om e. V

Assertion

Ref	Expression
inf0	|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))

Distinct variable group:   x,y,z,w

Proof of Theorem inf0

Step	Hyp	Ref	Expression
1		visset 1809	. . . 4 |- x e. V
2		fr0t 3943	. . . 4 |- (x e. V -> ((rec({<.v, u>. | u = suc v}, x) |` om)` (/)) = x)
3	1, 2	ax-mp 7	. . 3 |- ((rec({<.v, u>. | u = suc v}, x) |` om)` (/)) = x
4		frfnom 3942	. . . 4 |- (rec({<.v, u>. | u = suc v}, x) |` om) Fn om
5		peano1 3144	. . . 4 |- (/) e. om
6		fnfvelrn 3804	. . . 4 |- (((rec({<.v, u>. | u = suc v}, x) |` om) Fn om /\ (/) e. om) -> ((rec({<.v, u>. | u = suc v}, x) |` om)` (/)) e. ran (rec({<.v, u>. | u = suc v}, x) |` om))
7	4, 5, 6	mp2an 696	. . 3 |- ((rec({<.v, u>. | u = suc v}, x) |` om)` (/)) e. ran (rec({<.v, u>. | u = suc v}, x) |` om)
8	3, 7	eqeltrr 1542	. 2 |- x e. ran (rec({<.v, u>. | u = suc v}, x) |` om)
9		fvelrnb 3751	. . . . 5 |- ((rec({<.v, u>. | u = suc v}, x) |` om) Fn om -> (z e. ran (rec({<.v, u>. | u = suc v}, x) |` om) <-> E.f e. om ((rec({<.v, u>. | u = suc v}, x) |` om)` f) = z))
10	4, 9	ax-mp 7	. . . 4 |- (z e. ran (rec({<.v, u>. | u = suc v}, x) |` om) <-> E.f e. om ((rec({<.v, u>. | u = suc v}, x) |` om)` f) = z)
11		eleq1 1531	. . . . . . . 8 |- (((rec({<.v, u>. | u = suc v}, x) |` om)` f) = z -> (((rec({<.v, u>. | u = suc v}, x) |` om)` f) e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) <-> z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f)))
12		fvex 3723	. . . . . . . . . . 11 |- ((rec({<.v, u>. | u = suc v}, x) |` om)` f) e. V
13	12	sucex 3045	. . . . . . . . . 10 |- suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f) e. V
14		ax-17 969	. . . . . . . . . . 11 |- (z e. x -> A.v z e. x)
15		ax-17 969	. . . . . . . . . . 11 |- (z e. f -> A.v z e. f)
16		hbopab1 2808	. . . . . . . . . . . . . . 15 |- (z e. {<.v, u>. | u = suc v} -> A.v z e. {<.v, u>. | u = suc v})
17	16, 14	hbrdg 3927	. . . . . . . . . . . . . 14 |- (z e. rec({<.v, u>. | u = suc v}, x) -> A.v z e. rec({<.v, u>. | u = suc v}, x))
18		ax-17 969	. . . . . . . . . . . . . 14 |- (z e. om -> A.v z e. om)
19	17, 18	hbres 3362	. . . . . . . . . . . . 13 |- (z e. (rec({<.v, u>. | u = suc v}, x) |` om) -> A.v z e. (rec({<.v, u>. | u = suc v}, x) |` om))
20	19, 15	hbfv 3720	. . . . . . . . . . . 12 |- (z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` f) -> A.v z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` f))
21	20	hbsuc 3035	. . . . . . . . . . 11 |- (z e. suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f) -> A.v z e. suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f))
22		eqid 1473	. . . . . . . . . . 11 |- (rec({<.v, u>. | u = suc v}, x) |` om) = (rec({<.v, u>. | u = suc v}, x) |` om)
23		suceq 3029	. . . . . . . . . . 11 |- (v = ((rec({<.v, u>. | u = suc v}, x) |` om)` f) -> suc v = suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f))
24	14, 15, 21, 22, 23	frsucopab 3945	. . . . . . . . . 10 |- ((f e. om /\ suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f) e. V) -> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) = suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f))
25	13, 24	mpan2 695	. . . . . . . . 9 |- (f e. om -> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) = suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f))
26	12	sucid 3046	. . . . . . . . 9 |- ((rec({<.v, u>. | u = suc v}, x) |` om)` f) e. suc ((rec({<.v, u>. | u = suc v}, x) |` om)` f)
27	25, 26	syl5eleqr 1552	. . . . . . . 8 |- (f e. om -> ((rec({<.v, u>. | u = suc v}, x) |` om)` f) e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f))
28	11, 27	syl5bi 208	. . . . . . 7 |- (((rec({<.v, u>. | u = suc v}, x) |` om)` f) = z -> (f e. om -> z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f)))
29		peano2b 3142	. . . . . . . . 9 |- (f e. om <-> suc f e. om)
30		fnfvelrn 3804	. . . . . . . . . 10 |- (((rec({<.v, u>. | u = suc v}, x) |` om) Fn om /\ suc f e. om) -> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. ran (rec({<.v, u>. | u = suc v}, x) |` om))
31	4, 30	mpan 694	. . . . . . . . 9 |- (suc f e. om -> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. ran (rec({<.v, u>. | u = suc v}, x) |` om))
32	29, 31	sylbi 199	. . . . . . . 8 |- (f e. om -> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. ran (rec({<.v, u>. | u = suc v}, x) |` om))
33	32	a1i 8	. . . . . . 7 |- (((rec({<.v, u>. | u = suc v}, x) |` om)` f) = z -> (f e. om -> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. ran (rec({<.v, u>. | u = suc v}, x) |` om)))
34	28, 33	jcad 599	. . . . . 6 |- (((rec({<.v, u>. | u = suc v}, x) |` om)` f) = z -> (f e. om -> (z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) /\ ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. ran (rec({<.v, u>. | u = suc v}, x) |` om))))
35		fvex 3723	. . . . . . 7 |- ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. V
36		eleq2 1532	. . . . . . . 8 |- (w = ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) -> (z e. w <-> z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f)))
37		eleq1 1531	. . . . . . . 8 |- (w = ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) -> (w e. ran (rec({<.v, u>. | u = suc v}, x) |` om) <-> ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) e. ran (rec({<.v, u>. | u = suc v}, x) |` om)))
38	36, 37	anbi12d 627	. . . . . . 7 |- (w = ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) -> ((z e. w /\ w e. ran (rec({<.v, u>. | u = suc v}, x) |` om)) <-> (z e. ((rec({<.v, u>. | u = suc v}, x) |` om)` suc f) /\ ((rec({<.v, u>. | u = suc v},