Metamath Proof Explorer

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 ⊢ ω ∈ V → ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y

Proof

Step Hyp Ref Expression
1 fr0g ⊢ x ∈ V → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ ∅ = x
2 1 elv ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ ∅ = x
3 frfnom ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω Fn ω
4 peano1 ⊢ ∅ ∈ ω
5 fnfvelrn ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω Fn ω ∧ ∅ ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ ∅ ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
6 3 4 5 mp2an ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ ∅ ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
7 2 6 eqeltrri ⊢ x ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
8 fvelrnb ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω Fn ω → z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ↔ ∃ f ∈ ω rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z
9 3 8 ax-mp ⊢ z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ↔ ∃ f ∈ ω rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z
10 fvex ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f ∈ V
11 10 sucid ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f ∈ suc ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f
12 10 sucex ⊢ suc ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f ∈ V
13 eqid ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω = rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
14 suceq ⊢ z = v → suc ⁡ z = suc ⁡ v
15 suceq ⊢ z = rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f → suc ⁡ z = suc ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f
16 13 14 15 frsucmpt2 ⊢ f ∈ ω ∧ suc ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f ∈ V → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f = suc ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f
17 12 16 mpan2 ⊢ f ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f = suc ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f
18 11 17 eleqtrrid ⊢ f ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f
19 eleq1 ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ↔ z ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f
20 18 19 imbitrid ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z → f ∈ ω → z ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f
21 peano2b ⊢ f ∈ ω ↔ suc ⁡ f ∈ ω
22 fnfvelrn ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω Fn ω ∧ suc ⁡ f ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
23 3 22 mpan ⊢ suc ⁡ f ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
24 21 23 sylbi ⊢ f ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
25 20 24 jca2 ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z → f ∈ ω → z ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∧ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
26 fvex ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ V
27 eleq2 ⊢ w = rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f → z ∈ w ↔ z ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f
28 eleq1 ⊢ w = rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f → w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ↔ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
29 27 28 anbi12d ⊢ w = rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f → z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ↔ z ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∧ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
30 26 29 spcev ⊢ z ∈ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∧ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ suc ⁡ f ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
31 25 30 syl6com ⊢ f ∈ ω → rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
32 31 rexlimiv ⊢ ∃ f ∈ ω rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ⁡ f = z → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
33 9 32 sylbi ⊢ z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
34 33 ax-gen ⊢ ∀ z z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
35 fndm ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω Fn ω → dom ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω = ω
36 3 35 ax-mp ⊢ dom ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω = ω
37 id ⊢ ω ∈ V → ω ∈ V
38 36 37 eqeltrid ⊢ ω ∈ V → dom ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∈ V
39 fnfun ⊢ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω Fn ω → Fun ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
40 3 39 ax-mp ⊢ Fun ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
41 funrnex ⊢ dom ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∈ V → Fun ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∈ V
42 38 40 41 mpisyl ⊢ ω ∈ V → ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∈ V
43 eleq2 ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → x ∈ y ↔ x ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
44 eleq2 ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → z ∈ y ↔ z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
45 eleq2 ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → w ∈ y ↔ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
46 45 anbi2d ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → z ∈ w ∧ w ∈ y ↔ z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
47 46 exbidv ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ y ↔ ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
48 44 47 imbi12d ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
49 48 albidv ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ ∀ z z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
50 43 49 anbi12d ⊢ y = ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y ↔ x ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∧ ∀ z z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω
51 50 spcegv ⊢ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∈ V → x ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∧ ∀ z z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y
52 42 51 syl ⊢ ω ∈ V → x ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω ∧ ∀ z z ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ w z ∈ w ∧ w ∈ ran ⁡ rec ⁡ v ∈ V ⟼ suc ⁡ v x ↾ ω → ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y
53 7 34 52 mp2ani ⊢ ω ∈ V → ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ w z ∈ w ∧ w ∈ y