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

Theorem frecfcllem 6185
Description: Lemma for frecfcl 6186. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.)
Hypothesis
Ref Expression
frecfcllem.g 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
Assertion
Ref Expression
frecfcllem ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
Distinct variable groups:   𝐴,𝑔,𝑚,𝑥   𝑔,𝐹,𝑚,𝑥   𝑧,𝐹,𝑚,𝑥   𝑆,𝑚,𝑥,𝑧
Allowed substitution hints:   𝐴(𝑧)   𝑆(𝑔)   𝐺(𝑥,𝑧,𝑔,𝑚)

Proof of Theorem frecfcllem
Dummy variables 𝑓 𝑦 𝑘 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frecfcllem.g . . . . . 6 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
2 funmpt 5067 . . . . . . 7 Fun (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
32a1i 9 . . . . . 6 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) → Fun (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
4 ordom 4436 . . . . . . 7 Ord ω
54a1i 9 . . . . . 6 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) → Ord ω)
6 vex 2625 . . . . . . . 8 𝑓 ∈ V
7 simp2 945 . . . . . . . . 9 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑦 ∈ ω)
8 simp3 946 . . . . . . . . 9 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓:𝑦𝑆)
9 simp1ll 1007 . . . . . . . . . 10 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
10 fveq2 5320 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
1110eleq1d 2157 . . . . . . . . . . 11 (𝑧 = 𝑤 → ((𝐹𝑧) ∈ 𝑆 ↔ (𝐹𝑤) ∈ 𝑆))
1211cbvralv 2593 . . . . . . . . . 10 (∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆 ↔ ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
139, 12sylib 121 . . . . . . . . 9 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑤𝑆 (𝐹𝑤) ∈ 𝑆)
14 simp1lr 1008 . . . . . . . . 9 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝐴𝑆)
157, 8, 13, 14frecabcl 6180 . . . . . . . 8 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
16 dmeq 4651 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
1716eqeq1d 2097 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
18 fveq1 5319 . . . . . . . . . . . . . . 15 (𝑔 = 𝑓 → (𝑔𝑚) = (𝑓𝑚))
1918fveq2d 5324 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → (𝐹‘(𝑔𝑚)) = (𝐹‘(𝑓𝑚)))
2019eleq2d 2158 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓𝑚))))
2117, 20anbi12d 458 . . . . . . . . . . . 12 (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
2221rexbidv 2382 . . . . . . . . . . 11 (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
2316eqeq1d 2097 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
2423anbi1d 454 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥𝐴)))
2522, 24orbi12d 743 . . . . . . . . . 10 (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))))
2625abbidv 2206 . . . . . . . . 9 (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
27 eqid 2089 . . . . . . . . 9 (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
2826, 27fvmptg 5395 . . . . . . . 8 ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
296, 15, 28sylancr 406 . . . . . . 7 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
3029, 15eqeltrd 2165 . . . . . 6 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘𝑓) ∈ 𝑆)
31 limom 4443 . . . . . . . . . 10 Lim ω
32 limuni 4234 . . . . . . . . . 10 (Lim ω → ω = ω)
3331, 32ax-mp 7 . . . . . . . . 9 ω = ω
3433eleq2i 2155 . . . . . . . 8 (𝑦 ∈ ω ↔ 𝑦 ω)
35 peano2 4425 . . . . . . . 8 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
3634, 35sylbir 134 . . . . . . 7 (𝑦 ω → suc 𝑦 ∈ ω)
3736adantl 272 . . . . . 6 ((((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) ∧ 𝑦 ω) → suc 𝑦 ∈ ω)
3833eleq2i 2155 . . . . . . . 8 (𝑘 ∈ ω ↔ 𝑘 ω)
3938biimpi 119 . . . . . . 7 (𝑘 ∈ ω → 𝑘 ω)
4039adantl 272 . . . . . 6 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) → 𝑘 ω)
411, 3, 5, 30, 37, 40tfrcldm 6144 . . . . 5 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom 𝐺)
421, 3, 5, 30, 37, 40tfrcl 6145 . . . . 5 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ∈ 𝑆)
4341, 42jca 301 . . . 4 (((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) ∧ 𝑘 ∈ ω) → (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑆))
4443ralrimiva 2447 . . 3 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → ∀𝑘 ∈ ω (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑆))
45 tfrfun 6101 . . . . 5 Fun recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
461funeqi 5051 . . . . 5 (Fun 𝐺 ↔ Fun recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
4745, 46mpbir 145 . . . 4 Fun 𝐺
48 ffvresb 5477 . . . 4 (Fun 𝐺 → ((𝐺 ↾ ω):ω⟶𝑆 ↔ ∀𝑘 ∈ ω (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑆)))
4947, 48ax-mp 7 . . 3 ((𝐺 ↾ ω):ω⟶𝑆 ↔ ∀𝑘 ∈ ω (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑆))
5044, 49sylibr 133 . 2 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → (𝐺 ↾ ω):ω⟶𝑆)
51 df-frec 6172 . . . 4 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
521reseq1i 4724 . . . 4 (𝐺 ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
5351, 52eqtr4i 2112 . . 3 frec(𝐹, 𝐴) = (𝐺 ↾ ω)
5453feq1i 5169 . 2 (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (𝐺 ↾ ω):ω⟶𝑆)
5550, 54sylibr 133 1 ((∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆𝐴𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wo 665  w3a 925   = wceq 1290  wcel 1439  {cab 2075  wral 2360  wrex 2361  Vcvv 2622  c0 3289   cuni 3661  cmpt 3907  Ord word 4200  Lim wlim 4202  suc csuc 4203  ωcom 4420  dom cdm 4454  cres 4456  Fun wfun 5024  wf 5026  cfv 5030  recscrecs 6085  freccfrec 6171
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3962  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-iinf 4418
This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2624  df-sbc 2844  df-csb 2937  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-iun 3740  df-br 3854  df-opab 3908  df-mpt 3909  df-tr 3945  df-id 4131  df-iord 4204  df-on 4206  df-ilim 4207  df-suc 4209  df-iom 4421  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-f1 5035  df-fo 5036  df-f1o 5037  df-fv 5038  df-recs 6086  df-frec 6172
This theorem is referenced by:  frecfcl  6186
  Copyright terms: Public domain W3C validator