This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ω ∈ 𝑉 → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )

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 ⊢ ( ω ∈ 𝑉 → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )