Theorem inf0

Description: Existence of _om implies our axiom of infinity ax-inf . 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) Revised to closed form. (Revised by BJ, 20-May-2024)

	Ref	Expression
Assertion	inf0	⊢ ( ω ∈ 𝑉 → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fr0g	⊢ ( 𝑥 ∈ V → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) = 𝑥 )
2	1	elv	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) = 𝑥
3		frfnom	⊢ ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω
4		peano1	⊢ ∅ ∈ ω
5		fnfvelrn	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
6	3 4 5	mp2an	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
7	2 6	eqeltrri	⊢ 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
8		fvelrnb	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω → ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ↔ ∃ 𝑓 ∈ ω ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 ) )
9	3 8	ax-mp	⊢ ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ↔ ∃ 𝑓 ∈ ω ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 )
10		fvex	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ V
11	10	sucid	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 )
12	10	sucex	⊢ suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ V
13		eqid	⊢ ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
14		suceq	⊢ ( 𝑧 = 𝑣 → suc 𝑧 = suc 𝑣 )
15		suceq	⊢ ( 𝑧 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) → suc 𝑧 = suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) )
16	13 14 15	frsucmpt2	⊢ ( ( 𝑓 ∈ ω ∧ suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ V ) → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) = suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) )
17	12 16	mpan2	⊢ ( 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) = suc ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) )
18	11 17	eleqtrrid	⊢ ( 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) )
19		eleq1	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ↔ 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ) )
20	18 19	imbitrid	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ( 𝑓 ∈ ω → 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ) )
21		peano2b	⊢ ( 𝑓 ∈ ω ↔ suc 𝑓 ∈ ω )
22		fnfvelrn	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω ∧ suc 𝑓 ∈ ω ) → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
23	3 22	mpan	⊢ ( suc 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
24	21 23	sylbi	⊢ ( 𝑓 ∈ ω → ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
25	20 24	jca2	⊢ ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ( 𝑓 ∈ ω → ( 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∧ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
26		fvex	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ V
27		eleq2	⊢ ( 𝑤 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ) )
28		eleq1	⊢ ( 𝑤 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) → ( 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ↔ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
29	27 28	anbi12d	⊢ ( 𝑤 = ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ↔ ( 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∧ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
30	26 29	spcev	⊢ ( ( 𝑧 ∈ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∧ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ suc 𝑓 ) ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
31	25 30	syl6com	⊢ ( 𝑓 ∈ ω → ( ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) )
32	31	rexlimiv	⊢ ( ∃ 𝑓 ∈ ω ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ‘ 𝑓 ) = 𝑧 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
33	9 32	sylbi	⊢ ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
34	33	ax-gen	⊢ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) )
35		fndm	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω → dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) = ω )
36	3 35	ax-mp	⊢ dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) = ω
37		id	⊢ ( ω ∈ 𝑉 → ω ∈ 𝑉 )
38	36 37	eqeltrid	⊢ ( ω ∈ 𝑉 → dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ 𝑉 )
39		fnfun	⊢ ( ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) Fn ω → Fun ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) )
40	3 39	ax-mp	⊢ Fun ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω )
41		funrnex	⊢ ( dom ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ 𝑉 → ( Fun ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ V ) )
42	38 40 41	mpisyl	⊢ ( ω ∈ 𝑉 → 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	50	spcegv	⊢ ( ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∈ V → ( ( 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∧ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) ) )
52	42 51	syl	⊢ ( ω ∈ 𝑉 → ( ( 𝑥 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ∧ ∀ 𝑧 ( 𝑧 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran ( rec ( ( 𝑣 ∈ V ↦ suc 𝑣 ) , 𝑥 ) ↾ ω ) ) ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) ) )
53	7 34 52	mp2ani	⊢ ( ω ∈ 𝑉 → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )