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→∃yx∈y∧∀zz∈y→∃wz∈w∧w∈y

Proof

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