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) |` om)" 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	|- om e. V

Assertion

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

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

Proof of Theorem inf0

Step	Hyp	Ref	Expression
1		visset 1350	. . . . 5 |- y e. V
2		frzer 2990	. . . . 5 |- (y e. V -> ((rec({<.w, v>. | v = suc w}, y) |` om)` (/)) = y)
3	1, 2	ax-mp 6	. . . 4 |- ((rec({<.w, v>. | v = suc w}, y) |` om)` (/)) = y
4		frfnom 2989	. . . . 5 |- (rec({<.w, v>. | v = suc w}, y) |` om) Fn om
5		peano1 2390	. . . . 5 |- (/) e. om
6		fnfvrn 2889	. . . . 5 |- (((rec({<.w, v>. | v = suc w}, y) |` om) Fn om /\ (/) e. om) -> ((rec({<.w, v>. | v = suc w}, y) |` om)` (/)) e. ran (rec({<.w, v>. | v = suc w}, y) |` om))
7	4, 5, 6	mp2an 520	. . . 4 |- ((rec({<.w, v>. | v = suc w}, y) |` om)` (/)) e. ran (rec({<.w, v>. | v = suc w}, y) |` om)
8	3, 7	eqeltrr 1160	. . 3 |- y e. ran (rec({<.w, v>. | v = suc w}, y) |` om)
9		fvelrn 2883	. . . . . 6 |- ((rec({<.w, v>. | v = suc w}, y) |` om) Fn om -> (u e. ran (rec({<.w, v>. | v = suc w}, y) |` om) <-> E.f e. om ((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u))
10	4, 9	ax-mp 6	. . . . 5 |- (u e. ran (rec({<.w, v>. | v = suc w}, y) |` om) <-> E.f e. om ((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u)
11		eleq1 1149	. . . . . . . . . 10 |- (((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u -> (((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) <-> u e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f)))
12		fvex 2838	. . . . . . . . . . . 12 |- ((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. V
13	12	sucid 2304	. . . . . . . . . . 11 |- ((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f)
14	12	sucex 2303	. . . . . . . . . . . . 13 |- suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. V
15		ax-17 925	. . . . . . . . . . . . . 14 |- (z e. y -> A.w z e. y)
16		ax-17 925	. . . . . . . . . . . . . 14 |- (z e. f -> A.w z e. f)
17		hbopab1 2112	. . . . . . . . . . . . . . . . . 18 |- (z e. {<.w, v>. | v = suc w} -> A.w z e. {<.w, v>. | v = suc w})
18	17, 15	hbrdg 2974	. . . . . . . . . . . . . . . . 17 |- (z e. rec({<.w, v>. | v = suc w}, y) -> A.w z e. rec({<.w, v>. | v = suc w}, y))
19		ax-17 925	. . . . . . . . . . . . . . . . 17 |- (z e. om -> A.w z e. om)
20	18, 19	hbres 2577	. . . . . . . . . . . . . . . 16 |- (z e. (rec({<.w, v>. | v = suc w}, y) |` om) -> A.w z e. (rec({<.w, v>. | v = suc w}, y) |` om))
21	20, 16	hbfv 2837	. . . . . . . . . . . . . . 15 |- (z e. ((rec({<.w, v>. | v = suc w}, y) |` om)` f) -> A.w z e. ((rec({<.w, v>. | v = suc w}, y) |` om)` f))
22	21	hbsuc 2294	. . . . . . . . . . . . . 14 |- (z e. suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f) -> A.w z e. suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f))
23		cleqid 1102	. . . . . . . . . . . . . 14 |- (rec({<.w, v>. | v = suc w}, y) |` om) = (rec({<.w, v>. | v = suc w}, y) |` om)
24		suceq 2288	. . . . . . . . . . . . . 14 |- (w = ((rec({<.w, v>. | v = suc w}, y) |` om)` f) -> suc w = suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f))
25	15, 16, 22, 23, 24	frsucopab 2992	. . . . . . . . . . . . 13 |- ((f e. om /\ suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. V) -> ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) = suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f))
26	14, 25	mpan2 519	. . . . . . . . . . . 12 |- (f e. om -> ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) = suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f))
27	26	eleq2d 1156	. . . . . . . . . . 11 |- (f e. om -> (((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) <-> ((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. suc ((rec({<.w, v>. | v = suc w}, y) |` om)` f)))
28	13, 27	mpbiri 169	. . . . . . . . . 10 |- (f e. om -> ((rec({<.w, v>. | v = suc w}, y) |` om)` f) e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f))
29	11, 28	syl5bi 183	. . . . . . . . 9 |- (((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u -> (f e. om -> u e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f)))
30		peano2b 2388	. . . . . . . . . . 11 |- (f e. om <-> suc f e. om)
31		fnfvrn 2889	. . . . . . . . . . . 12 |- (((rec({<.w, v>. | v = suc w}, y) |` om) Fn om /\ suc f e. om) -> ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. ran (rec({<.w, v>. | v = suc w}, y) |` om))
32	4, 31	mpan 518	. . . . . . . . . . 11 |- (suc f e. om -> ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. ran (rec({<.w, v>. | v = suc w}, y) |` om))
33	30, 32	sylbi 174	. . . . . . . . . 10 |- (f e. om -> ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. ran (rec({<.w, v>. | v = suc w}, y) |` om))
34	33	a1i 7	. . . . . . . . 9 |- (((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u -> (f e. om -> ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. ran (rec({<.w, v>. | v = suc w}, y) |` om)))
35	29, 34	jcad 455	. . . . . . . 8 |- (((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u -> (f e. om -> (u e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) /\ ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. ran (rec({<.w, v>. | v = suc w}, y) |` om))))
36	35	com12 13	. . . . . . 7 |- (f e. om -> (((rec({<.w, v>. | v = suc w}, y) |` om)` f) = u -> (u e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) /\ ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. ran (rec({<.w, v>. | v = suc w}, y) |` om))))
37		fvex 2838	. . . . . . . 8 |- ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) e. V
38		eleq2 1150	. . . . . . . . 9 |- (z = ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f) -> (u e. z <-> u e. ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f)))
39		eleq1 1149	. . . . . . . . 9 |- (z = ((rec({<.w, v>. | v = suc w}, y) |` om)` suc f