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

Theorem inf0 9657
Description: Existence of ω implies our axiom of infinity ax-inf 9674. 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 9674. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.)
Assertion
Ref Expression
inf0 (ω ∈ 𝑉 → ∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem inf0
Dummy variables 𝑣 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fr0g 8472 . . . 4 (𝑥 ∈ V → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) = 𝑥)
21elv 3484 . . 3 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) = 𝑥
3 frfnom 8471 . . . 4 (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
4 peano1 7906 . . . 4 ∅ ∈ ω
5 fnfvelrn 7098 . . . 4 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
63, 4, 5mp2an 692 . . 3 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
72, 6eqeltrri 2837 . 2 𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
8 fvelrnb 6967 . . . . 5 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω → (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧))
93, 8ax-mp 5 . . . 4 (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧)
10 fvex 6917 . . . . . . . . . 10 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V
1110sucid 6464 . . . . . . . . 9 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓)
1210sucex 7822 . . . . . . . . . 10 suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V
13 eqid 2736 . . . . . . . . . . 11 (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) = (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
14 suceq 6448 . . . . . . . . . . 11 (𝑧 = 𝑣 → suc 𝑧 = suc 𝑣)
15 suceq 6448 . . . . . . . . . . 11 (𝑧 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) → suc 𝑧 = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓))
1613, 14, 15frsucmpt2 8476 . . . . . . . . . 10 ((𝑓 ∈ ω ∧ suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓))
1712, 16mpan2 691 . . . . . . . . 9 (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓))
1811, 17eleqtrrid 2847 . . . . . . . 8 (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓))
19 eleq1 2828 . . . . . . . 8 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ↔ 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)))
2018, 19imbitrid 244 . . . . . . 7 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)))
21 peano2b 7900 . . . . . . . 8 (𝑓 ∈ ω ↔ suc 𝑓 ∈ ω)
22 fnfvelrn 7098 . . . . . . . . 9 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω ∧ suc 𝑓 ∈ ω) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
233, 22mpan 690 . . . . . . . 8 (suc 𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
2421, 23sylbi 217 . . . . . . 7 (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
2520, 24jca2 513 . . . . . 6 (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → (𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
26 fvex 6917 . . . . . . 7 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ V
27 eleq2 2829 . . . . . . . 8 (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → (𝑧𝑤𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)))
28 eleq1 2828 . . . . . . . 8 (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → (𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
2927, 28anbi12d 632 . . . . . . 7 (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → ((𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) ↔ (𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
3026, 29spcev 3605 . . . . . 6 ((𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
3125, 30syl6com 37 . . . . 5 (𝑓 ∈ ω → (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
3231rexlimiv 3147 . . . 4 (∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
339, 32sylbi 217 . . 3 (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
3433ax-gen 1795 . 2 𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
35 fndm 6669 . . . . . 6 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω → dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) = ω)
363, 35ax-mp 5 . . . . 5 dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) = ω
37 id 22 . . . . 5 (ω ∈ 𝑉 → ω ∈ 𝑉)
3836, 37eqeltrid 2844 . . . 4 (ω ∈ 𝑉 → dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ 𝑉)
39 fnfun 6666 . . . . 5 ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) Fn ω → Fun (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))
403, 39ax-mp 5 . . . 4 Fun (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)
41 funrnex 7974 . . . 4 (dom (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ 𝑉 → (Fun (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V))
4238, 40, 41mpisyl 21 . . 3 (ω ∈ 𝑉 → ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V)
43 eleq2 2829 . . . . 5 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑥𝑦𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
44 eleq2 2829 . . . . . . 7 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑧𝑦𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
45 eleq2 2829 . . . . . . . . 9 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑤𝑦𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))
4645anbi2d 630 . . . . . . . 8 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑧𝑤𝑤𝑦) ↔ (𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
4746exbidv 1921 . . . . . . 7 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (∃𝑤(𝑧𝑤𝑤𝑦) ↔ ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))
4844, 47imbi12d 344 . . . . . 6 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))))
4948albidv 1920 . . . . 5 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)) ↔ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))))
5043, 49anbi12d 632 . . . 4 (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))) ↔ (𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))))
5150spcegv 3596 . . 3 (ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈ V → ((𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) → ∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))))
5242, 51syl 17 . 2 (ω ∈ 𝑉 → ((𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧𝑤𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) → ∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦)))))
537, 34, 52mp2ani 698 1 (ω ∈ 𝑉 → ∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wex 1779  wcel 2108  wrex 3069  Vcvv 3479  c0 4332  cmpt 5223  dom cdm 5683  ran crn 5684  cres 5685  suc csuc 6384  Fun wfun 6553   Fn wfn 6554  cfv 6559  ωcom 7883  reccrdg 8445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pr 5430  ax-un 7751
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-ov 7432  df-om 7884  df-2nd 8011  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446
This theorem is referenced by:  axinf  9680
  Copyright terms: Public domain W3C validator