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