Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inf0 Structured version   Visualization version   GIF version

Theorem inf0 8693
 Description: Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class "ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) " exists, is a subset of its union, and contains a given set 𝑥 (and thus is nonempty). Thus, it provides an example demonstrating that a set 𝑦 exists with the necessary properties demanded by ax-inf 8710. (Contributed by NM, 15-Oct-1996.)
Hypothesis
Ref Expression
inf0.1 ω ∈ V
Assertion
Ref Expression
inf0 𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Proof of Theorem inf0
Dummy variables 𝑣 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3343 . . . 4 𝑥 ∈ V
2 fr0g 7701 . . . 4 (𝑥 ∈ V → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) = 𝑥)
31, 2ax-mp 5 . . 3 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) = 𝑥
4 frfnom 7700 . . . 4 (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
5 peano1 7251 . . . 4 ∅ ∈ ω
6 fnfvelrn 6520 . . . 4 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
74, 5, 6mp2an 710 . . 3 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
83, 7eqeltrri 2836 . 2 𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
9 fvelrnb 6406 . . . . 5 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω → (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧))
104, 9ax-mp 5 . . . 4 (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧)
11 fvex 6363 . . . . . . . . . 10 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V
1211sucid 5965 . . . . . . . . 9 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓)
1311sucex 7177 . . . . . . . . . 10 suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V
14 eqid 2760 . . . . . . . . . . 11 (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) = (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
15 suceq 5951 . . . . . . . . . . 11 (𝑧 = 𝑣 → suc 𝑧 = suc 𝑣)
16 suceq 5951 . . . . . . . . . . 11 (𝑧 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) → suc 𝑧 = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓))
1714, 15, 16frsucmpt2 7705 . . . . . . . . . 10 ((𝑓 ∈ ω ∧ suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓))
1813, 17mpan2 709 . . . . . . . . 9 (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓))
1912, 18syl5eleqr 2846 . . . . . . . 8 (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓))
20 eleq1 2827 . . . . . . . 8 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ↔ 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)))
2119, 20syl5ib 234 . . . . . . 7 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)))
22 peano2b 7247 . . . . . . . . 9 (𝑓 ∈ ω ↔ suc 𝑓 ∈ ω)
23 fnfvelrn 6520 . . . . . . . . . 10 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω ∧ suc 𝑓 ∈ ω) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
244, 23mpan 708 . . . . . . . . 9 (suc 𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
2522, 24sylbi 207 . . . . . . . 8 (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
2625a1i 11 . . . . . . 7 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
2721, 26jcad 556 . . . . . 6 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → (𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
28 fvex 6363 . . . . . . 7 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ V
29 eleq2 2828 . . . . . . . 8 (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → (𝑧𝑤𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)))
30 eleq1 2827 . . . . . . . 8 (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → (𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
3129, 30anbi12d 749 . . . . . . 7 (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → ((𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) ↔ (𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
3228, 31spcev 3440 . . . . . 6 ((𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
3327, 32syl6com 37 . . . . 5 (𝑓 ∈ ω → (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
3433rexlimiv 3165 . . . 4 (∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
3510, 34sylbi 207 . . 3 (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
3635ax-gen 1871 . 2 𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
37 fndm 6151 . . . . . 6 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω → dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) = ω)
384, 37ax-mp 5 . . . . 5 dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) = ω
39 inf0.1 . . . . 5 ω ∈ V
4038, 39eqeltri 2835 . . . 4 dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V
41 fnfun 6149 . . . . 5 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω → Fun (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
424, 41ax-mp 5 . . . 4 Fun (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
43 funrnex 7299 . . . 4 (dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V → (Fun (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V))
4440, 42, 43mp2 9 . . 3 ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V
45 eleq2 2828 . . . 4 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑥𝑦𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
46 eleq2 2828 . . . . . 6 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑧𝑦𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
47 eleq2 2828 . . . . . . . 8 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑤𝑦𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
4847anbi2d 742 . . . . . . 7 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑧𝑤𝑤𝑦) ↔ (𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
4948exbidv 1999 . . . . . 6 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (∃𝑤(𝑧𝑤𝑤𝑦) ↔ ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
5046, 49imbi12d 333 . . . . 5 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))))
5150albidv 1998 . . . 4 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))))
5245, 51anbi12d 749 . . 3 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ (𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))))
5344, 52spcev 3440 . 2 ((𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) → ∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))))
548, 36, 53mp2an 710 1 𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1630   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∃wrex 3051  Vcvv 3340  ∅c0 4058   ↦ cmpt 4881  dom cdm 5266  ran crn 5267   ↾ cres 5268  suc csuc 5886  Fun wfun 6043   Fn wfn 6044  ‘cfv 6049  ωcom 7231  reccrdg 7675 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676 This theorem is referenced by:  axinf  8716
 Copyright terms: Public domain W3C validator