Theorem inf0

Description: Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class " ` ran ( rec ( ( v e.V |-> suc v ) , x ) |`om ) " exists, is a subset of its union, and contains a given set x (and thus is nonempty). Thus, it provides an example demonstrating that a set y exists with the necessary properties demanded by ax-inf . (Contributed by NM, 15-Oct-1996)

	Ref	Expression
Hypothesis	inf0.1	⊢ ω ∈ V
Assertion	inf0	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		inf0.1	⊢ ω ∈ V
2		fr0g	⊢ ( 𝑥 ∈ V → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) = 𝑥 )
3	2	elv	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) = 𝑥
4		frfnom	⊢ ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω
5		peano1	⊢ ∅ ∈ ω
6		fnfvelrn	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
7	4 5 6	mp2an	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
8	3 7	eqeltrri	⊢ 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
9		fvelrnb	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω → ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ↔ ∃ 𝑓 ∈ ω ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 ) )
10	4 9	ax-mp	⊢ ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ↔ ∃ 𝑓 ∈ ω ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 )
11		fvex	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ V
12	11	sucid	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 )
13	11	sucex	⊢ suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ V
14		eqid	⊢ ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
15		suceq	⊢ ( 𝑧 = 𝑣 → suc 𝑧 = suc 𝑣 )
16		suceq	⊢ ( 𝑧 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) → suc 𝑧 = suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) )
17	14 15 16	frsucmpt2	⊢ ( ( 𝑓 ∈ ω ∧ suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ V ) → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) = suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) )
18	13 17	mpan2	⊢ ( 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) = suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) )
19	12 18	eleqtrrid	⊢ ( 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) )
20		eleq1	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ↔ 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ) )
21	19 20	syl5ib	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ( 𝑓 ∈ ω → 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ) )
22		peano2b	⊢ ( 𝑓 ∈ ω ↔ suc 𝑓 ∈ ω )
23		fnfvelrn	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω ∧ suc 𝑓 ∈ ω ) → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
24	4 23	mpan	⊢ ( suc 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
25	22 24	sylbi	⊢ ( 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
26	21 25	jca2	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ( 𝑓 ∈ ω → ( 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∧ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
27		fvex	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ V
28		eleq2	⊢ ( 𝑤 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ) )
29		eleq1	⊢ ( 𝑤 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) → ( 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ↔ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
30	28 29	anbi12d	⊢ ( 𝑤 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ↔ ( 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∧ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
31	27 30	spcev	⊢ ( ( 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∧ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
32	26 31	syl6com	⊢ ( 𝑓 ∈ ω → ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
33	32	rexlimiv	⊢ ( ∃ 𝑓 ∈ ω ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
34	10 33	sylbi	⊢ ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
35	34	ax-gen	⊢ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
36		fndm	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω → dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) = ω )
37	4 36	ax-mp	⊢ dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) = ω
38	37 1	eqeltri	⊢ dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ V
39		fnfun	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω → Fun ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
40	4 39	ax-mp	⊢ Fun ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
41		funrnex	⊢ ( dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ V → ( Fun ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ V ) )
42	38 40 41	mp2	⊢ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ V
43		eleq2	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
44		eleq2	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
45		eleq2	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( 𝑤 ∈ 𝑦 ↔ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
46	45	anbi2d	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
47	46	exbidv	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
48	44 47	imbi12d	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) ) )
49	48	albidv	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) ) )
50	43 49	anbi12d	⊢ ( 𝑦 = ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∧ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) ) ) )
51	42 50	spcev	⊢ ( ( 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∧ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
52	8 35 51	mp2an	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )