ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfr1onlemres GIF version

Theorem tfr1onlemres 6070
Description: Lemma for tfr1on 6071. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.)
Hypotheses
Ref Expression
tfr1on.f 𝐹 = recs(𝐺)
tfr1on.g (𝜑 → Fun 𝐺)
tfr1on.x (𝜑 → Ord 𝑋)
tfr1on.ex ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
tfr1onlemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfr1onlemres.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfr1onlemres.yx (𝜑𝑌𝑋)
Assertion
Ref Expression
tfr1onlemres (𝜑𝑌 ⊆ dom 𝐹)
Distinct variable groups:   𝑥,𝐴   𝑓,𝐺,𝑥,𝑦   𝑓,𝑋,𝑥   𝑓,𝑌,𝑥   𝜑,𝑓,𝑥
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦,𝑓)   𝐹(𝑥,𝑦,𝑓)   𝑋(𝑦)   𝑌(𝑦)

Proof of Theorem tfr1onlemres
Dummy variables 𝑔 𝑧 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfr1on.x . . . . . . . . . 10 (𝜑 → Ord 𝑋)
21adantr 270 . . . . . . . . 9 ((𝜑𝑧𝑌) → Ord 𝑋)
3 simpr 108 . . . . . . . . . 10 ((𝜑𝑧𝑌) → 𝑧𝑌)
4 tfr1onlemres.yx . . . . . . . . . . 11 (𝜑𝑌𝑋)
54adantr 270 . . . . . . . . . 10 ((𝜑𝑧𝑌) → 𝑌𝑋)
63, 5jca 300 . . . . . . . . 9 ((𝜑𝑧𝑌) → (𝑧𝑌𝑌𝑋))
7 ordtr1 4191 . . . . . . . . 9 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
82, 6, 7sylc 61 . . . . . . . 8 ((𝜑𝑧𝑌) → 𝑧𝑋)
9 tfr1on.f . . . . . . . . 9 𝐹 = recs(𝐺)
10 tfr1on.g . . . . . . . . 9 (𝜑 → Fun 𝐺)
11 tfr1on.ex . . . . . . . . 9 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
12 tfr1onlemsucfn.1 . . . . . . . . 9 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
13 tfr1onlemres.u . . . . . . . . 9 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
149, 10, 1, 11, 12, 13tfr1onlemaccex 6069 . . . . . . . 8 ((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
158, 14syldan 276 . . . . . . 7 ((𝜑𝑧𝑌) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
1610ad2antrr 472 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → Fun 𝐺)
171ad2antrr 472 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → Ord 𝑋)
18113adant1r 1165 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ 𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
19183adant1r 1165 . . . . . . . . 9 ((((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ∧ 𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
204ad2antrr 472 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑌𝑋)
213adantr 270 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑧𝑌)
2213adantlr 461 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
2322adantlr 461 . . . . . . . . 9 ((((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
24 simprl 498 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑔 Fn 𝑧)
25 fneq2 5070 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑔 Fn 𝑤𝑔 Fn 𝑧))
26 raleq 2558 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
2725, 26anbi12d 457 . . . . . . . . . . . 12 (𝑤 = 𝑧 → ((𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
2827rspcev 2715 . . . . . . . . . . 11 ((𝑧𝑋 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ∃𝑤𝑋 (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
298, 28sylan 277 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ∃𝑤𝑋 (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
30 vex 2618 . . . . . . . . . . 11 𝑔 ∈ V
3112tfr1onlem3ag 6058 . . . . . . . . . . 11 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑤𝑋 (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
3230, 31ax-mp 7 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑤𝑋 (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
3329, 32sylibr 132 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑔𝐴)
349, 16, 17, 19, 12, 20, 21, 23, 24, 33tfr1onlemsucaccv 6062 . . . . . . . 8 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
35 vex 2618 . . . . . . . . . . 11 𝑧 ∈ V
36 fneq2 5070 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝑔 Fn 𝑥𝑔 Fn 𝑧))
3736imbi1d 229 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑔 Fn 𝑥 → (𝐺𝑔) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V)))
38113expia 1143 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
3938alrimiv 1799 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
40 fneq1 5069 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑔 → (𝑓 Fn 𝑥𝑔 Fn 𝑥))
41 fveq2 5270 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
4241eleq1d 2153 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ V ↔ (𝐺𝑔) ∈ V))
4340, 42imbi12d 232 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑔 → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ (𝑔 Fn 𝑥 → (𝐺𝑔) ∈ V)))
4443spv 1785 . . . . . . . . . . . . . . . . 17 (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) → (𝑔 Fn 𝑥 → (𝐺𝑔) ∈ V))
4539, 44syl 14 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → (𝑔 Fn 𝑥 → (𝐺𝑔) ∈ V))
4645ralrimiva 2442 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝑋 (𝑔 Fn 𝑥 → (𝐺𝑔) ∈ V))
4746adantr 270 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑌) → ∀𝑥𝑋 (𝑔 Fn 𝑥 → (𝐺𝑔) ∈ V))
4837, 47, 8rspcdva 2720 . . . . . . . . . . . . 13 ((𝜑𝑧𝑌) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
4948imp 122 . . . . . . . . . . . 12 (((𝜑𝑧𝑌) ∧ 𝑔 Fn 𝑧) → (𝐺𝑔) ∈ V)
5024, 49syldan 276 . . . . . . . . . . 11 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝐺𝑔) ∈ V)
51 opexg 4031 . . . . . . . . . . 11 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
5235, 50, 51sylancr 405 . . . . . . . . . 10 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
53 snidg 3458 . . . . . . . . . 10 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
54 elun2 3157 . . . . . . . . . 10 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
5552, 53, 543syl 17 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
56 opeldmg 4611 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → (⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
5735, 50, 56sylancr 405 . . . . . . . . 9 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
5855, 57mpd 13 . . . . . . . 8 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
59 dmeq 4606 . . . . . . . . . 10 ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → dom = dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
6059eleq2d 2154 . . . . . . . . 9 ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑧 ∈ dom 𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
6160rspcev 2715 . . . . . . . 8 (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴𝑧 ∈ dom (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝐴 𝑧 ∈ dom )
6234, 58, 61syl2anc 403 . . . . . . 7 (((𝜑𝑧𝑌) ∧ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ∃𝐴 𝑧 ∈ dom )
6315, 62exlimddv 1823 . . . . . 6 ((𝜑𝑧𝑌) → ∃𝐴 𝑧 ∈ dom )
64 eliun 3719 . . . . . 6 (𝑧 𝐴 dom ↔ ∃𝐴 𝑧 ∈ dom )
6563, 64sylibr 132 . . . . 5 ((𝜑𝑧𝑌) → 𝑧 𝐴 dom )
6665ex 113 . . . 4 (𝜑 → (𝑧𝑌𝑧 𝐴 dom ))
6766ssrdv 3020 . . 3 (𝜑𝑌 𝐴 dom )
68 dmuni 4616 . . . 4 dom 𝐴 = 𝐴 dom
6912, 1tfr1onlemssrecs 6060 . . . . 5 (𝜑 𝐴 ⊆ recs(𝐺))
70 dmss 4605 . . . . 5 ( 𝐴 ⊆ recs(𝐺) → dom 𝐴 ⊆ dom recs(𝐺))
7169, 70syl 14 . . . 4 (𝜑 → dom 𝐴 ⊆ dom recs(𝐺))
7268, 71syl5eqssr 3060 . . 3 (𝜑 𝐴 dom ⊆ dom recs(𝐺))
7367, 72sstrd 3024 . 2 (𝜑𝑌 ⊆ dom recs(𝐺))
749dmeqi 4607 . 2 dom 𝐹 = dom recs(𝐺)
7573, 74syl6sseqr 3062 1 (𝜑𝑌 ⊆ dom 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 922  wal 1285   = wceq 1287  wex 1424  wcel 1436  {cab 2071  wral 2355  wrex 2356  Vcvv 2615  cun 2986  wss 2988  {csn 3431  cop 3434   cuni 3638   ciun 3715  Ord word 4165  suc csuc 4168  dom cdm 4413  cres 4415  Fun wfun 4977   Fn wfn 4978  cfv 4983  recscrecs 6025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3931  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-id 4096  df-iord 4169  df-on 4171  df-suc 4174  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-recs 6026
This theorem is referenced by:  tfr1on  6071
  Copyright terms: Public domain W3C validator