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

Theorem tfrlem16 7188
 Description: Lemma for finite recursion. Without assuming ax-rep 4548, we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014.)
Hypothesis
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Assertion
Ref Expression
tfrlem16 Lim dom recs(𝐹)
Distinct variable group:   𝑥,𝑓,𝑦,𝐹
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑓)

Proof of Theorem tfrlem16
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . . 4 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
21tfrlem8 7179 . . 3 Ord dom recs(𝐹)
3 ordzsl 6749 . . 3 (Ord dom recs(𝐹) ↔ (dom recs(𝐹) = ∅ ∨ ∃𝑧 ∈ On dom recs(𝐹) = suc 𝑧 ∨ Lim dom recs(𝐹)))
42, 3mpbi 215 . 2 (dom recs(𝐹) = ∅ ∨ ∃𝑧 ∈ On dom recs(𝐹) = suc 𝑧 ∨ Lim dom recs(𝐹))
5 res0 5158 . . . . . . 7 (recs(𝐹) ↾ ∅) = ∅
6 0ex 4568 . . . . . . 7 ∅ ∈ V
75, 6eqeltri 2579 . . . . . 6 (recs(𝐹) ↾ ∅) ∈ V
8 0elon 5527 . . . . . . 7 ∅ ∈ On
91tfrlem15 7187 . . . . . . 7 (∅ ∈ On → (∅ ∈ dom recs(𝐹) ↔ (recs(𝐹) ↾ ∅) ∈ V))
108, 9ax-mp 5 . . . . . 6 (∅ ∈ dom recs(𝐹) ↔ (recs(𝐹) ↾ ∅) ∈ V)
117, 10mpbir 216 . . . . 5 ∅ ∈ dom recs(𝐹)
12 n0i 3762 . . . . 5 (∅ ∈ dom recs(𝐹) → ¬ dom recs(𝐹) = ∅)
1311, 12ax-mp 5 . . . 4 ¬ dom recs(𝐹) = ∅
1413pm2.21i 138 . . 3 (dom recs(𝐹) = ∅ → Lim dom recs(𝐹))
151tfrlem13 7185 . . . . 5 ¬ recs(𝐹) ∈ V
16 simpr 470 . . . . . . . . . 10 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → dom recs(𝐹) = suc 𝑧)
17 df-suc 5480 . . . . . . . . . 10 suc 𝑧 = (𝑧 ∪ {𝑧})
1816, 17syl6eq 2555 . . . . . . . . 9 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → dom recs(𝐹) = (𝑧 ∪ {𝑧}))
1918reseq2d 5154 . . . . . . . 8 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → (recs(𝐹) ↾ dom recs(𝐹)) = (recs(𝐹) ↾ (𝑧 ∪ {𝑧})))
201tfrlem6 7177 . . . . . . . . 9 Rel recs(𝐹)
21 resdm 5196 . . . . . . . . 9 (Rel recs(𝐹) → (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹))
2220, 21ax-mp 5 . . . . . . . 8 (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹)
23 resundi 5167 . . . . . . . 8 (recs(𝐹) ↾ (𝑧 ∪ {𝑧})) = ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧}))
2419, 22, 233eqtr3g 2562 . . . . . . 7 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → recs(𝐹) = ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧})))
25 vex 3069 . . . . . . . . . . 11 𝑧 ∈ V
2625sucid 5553 . . . . . . . . . 10 𝑧 ∈ suc 𝑧
2726, 16syl5eleqr 2590 . . . . . . . . 9 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → 𝑧 ∈ dom recs(𝐹))
281tfrlem9a 7181 . . . . . . . . 9 (𝑧 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝑧) ∈ V)
2927, 28syl 17 . . . . . . . 8 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → (recs(𝐹) ↾ 𝑧) ∈ V)
30 snex 4682 . . . . . . . . 9 {⟨𝑧, (recs(𝐹)‘𝑧)⟩} ∈ V
311tfrlem7 7178 . . . . . . . . . 10 Fun recs(𝐹)
32 funressn 6145 . . . . . . . . . 10 (Fun recs(𝐹) → (recs(𝐹) ↾ {𝑧}) ⊆ {⟨𝑧, (recs(𝐹)‘𝑧)⟩})
3331, 32ax-mp 5 . . . . . . . . 9 (recs(𝐹) ↾ {𝑧}) ⊆ {⟨𝑧, (recs(𝐹)‘𝑧)⟩}
3430, 33ssexi 4581 . . . . . . . 8 (recs(𝐹) ↾ {𝑧}) ∈ V
35 unexg 6669 . . . . . . . 8 (((recs(𝐹) ↾ 𝑧) ∈ V ∧ (recs(𝐹) ↾ {𝑧}) ∈ V) → ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧})) ∈ V)
3629, 34, 35sylancl 684 . . . . . . 7 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → ((recs(𝐹) ↾ 𝑧) ∪ (recs(𝐹) ↾ {𝑧})) ∈ V)
3724, 36eqeltrd 2583 . . . . . 6 ((𝑧 ∈ On ∧ dom recs(𝐹) = suc 𝑧) → recs(𝐹) ∈ V)
3837rexlimiva 2903 . . . . 5 (∃𝑧 ∈ On dom recs(𝐹) = suc 𝑧 → recs(𝐹) ∈ V)
3915, 38mto 183 . . . 4 ¬ ∃𝑧 ∈ On dom recs(𝐹) = suc 𝑧
4039pm2.21i 138 . . 3 (∃𝑧 ∈ On dom recs(𝐹) = suc 𝑧 → Lim dom recs(𝐹))
41 id 22 . . 3 (Lim dom recs(𝐹) → Lim dom recs(𝐹))
4214, 40, 413jaoi 1373 . 2 ((dom recs(𝐹) = ∅ ∨ ∃𝑧 ∈ On dom recs(𝐹) = suc 𝑧 ∨ Lim dom recs(𝐹)) → Lim dom recs(𝐹))
434, 42ax-mp 5 1 Lim dom recs(𝐹)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 191   ∧ wa 378   ∨ w3o 1020   = wceq 1468   ∈ wcel 1937  {cab 2491  ∀wral 2791  ∃wrex 2792  Vcvv 3066   ∪ cun 3424   ⊆ wss 3426  ∅c0 3757  {csn 3995  ⟨cop 4001  dom cdm 4880   ↾ cres 4882  Rel wrel 4885  Ord word 5473  Oncon0 5474  Lim wlim 5475  suc csuc 5476  Fun wfun 5627   Fn wfn 5628  ‘cfv 5633  recscrecs 7166 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659 This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-wrecs 7105  df-recs 7167 This theorem is referenced by:  tfr1a  7189
 Copyright terms: Public domain W3C validator