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

Theorem freccllem 6400
Description: Lemma for freccl 6401. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.)
Hypotheses
Ref Expression
freccl.a (𝜑𝐴𝑆)
freccl.cl ((𝜑𝑧𝑆) → (𝐹𝑧) ∈ 𝑆)
freccl.b (𝜑𝐵 ∈ ω)
freccllem.g 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
Assertion
Ref Expression
freccllem (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆)
Distinct variable groups:   𝐴,𝑔,𝑚,𝑥   𝑧,𝐴,𝑚,𝑥   𝑥,𝐵   𝑔,𝐹,𝑚,𝑥   𝑧,𝐹   𝑆,𝑚,𝑥,𝑧   𝜑,𝑚,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑔)   𝐵(𝑧,𝑔,𝑚)   𝑆(𝑔)   𝐺(𝑥,𝑧,𝑔,𝑚)

Proof of Theorem freccllem
Dummy variables 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-frec 6389 . . . 4 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
2 freccllem.g . . . . 5 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
32reseq1i 4902 . . . 4 (𝐺 ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
41, 3eqtr4i 2201 . . 3 frec(𝐹, 𝐴) = (𝐺 ↾ ω)
54fveq1i 5515 . 2 (frec(𝐹, 𝐴)‘𝐵) = ((𝐺 ↾ ω)‘𝐵)
6 freccl.b . . . 4 (𝜑𝐵 ∈ ω)
7 fvres 5538 . . . 4 (𝐵 ∈ ω → ((𝐺 ↾ ω)‘𝐵) = (𝐺𝐵))
86, 7syl 14 . . 3 (𝜑 → ((𝐺 ↾ ω)‘𝐵) = (𝐺𝐵))
9 funmpt 5253 . . . . 5 Fun (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
109a1i 9 . . . 4 (𝜑 → Fun (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
11 ordom 4605 . . . . 5 Ord ω
1211a1i 9 . . . 4 (𝜑 → Ord ω)
13 vex 2740 . . . . . 6 𝑓 ∈ V
14 simp2 998 . . . . . . 7 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑦 ∈ ω)
15 simp3 999 . . . . . . 7 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝑓:𝑦𝑆)
16 freccl.cl . . . . . . . . 9 ((𝜑𝑧𝑆) → (𝐹𝑧) ∈ 𝑆)
1716ralrimiva 2550 . . . . . . . 8 (𝜑 → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
18173ad2ant1 1018 . . . . . . 7 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ∀𝑧𝑆 (𝐹𝑧) ∈ 𝑆)
19 freccl.a . . . . . . . 8 (𝜑𝐴𝑆)
20193ad2ant1 1018 . . . . . . 7 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → 𝐴𝑆)
2114, 15, 18, 20frecabcl 6397 . . . . . 6 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆)
22 dmeq 4826 . . . . . . . . . . . 12 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
2322eqeq1d 2186 . . . . . . . . . . 11 (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
24 fveq1 5513 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → (𝑔𝑚) = (𝑓𝑚))
2524fveq2d 5518 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (𝐹‘(𝑔𝑚)) = (𝐹‘(𝑓𝑚)))
2625eleq2d 2247 . . . . . . . . . . 11 (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓𝑚))))
2723, 26anbi12d 473 . . . . . . . . . 10 (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
2827rexbidv 2478 . . . . . . . . 9 (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚)))))
2922eqeq1d 2186 . . . . . . . . . 10 (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
3029anbi1d 465 . . . . . . . . 9 (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥𝐴)))
3128, 30orbi12d 793 . . . . . . . 8 (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))))
3231abbidv 2295 . . . . . . 7 (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
33 eqid 2177 . . . . . . 7 (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
3432, 33fvmptg 5591 . . . . . 6 ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))} ∈ 𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
3513, 21, 34sylancr 414 . . . . 5 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚𝑥 ∈ (𝐹‘(𝑓𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥𝐴))})
3635, 21eqeltrd 2254 . . . 4 ((𝜑𝑦 ∈ ω ∧ 𝑓:𝑦𝑆) → ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})‘𝑓) ∈ 𝑆)
37 limom 4612 . . . . . . 7 Lim ω
38 limuni 4395 . . . . . . 7 (Lim ω → ω = ω)
3937, 38ax-mp 5 . . . . . 6 ω = ω
4039eleq2i 2244 . . . . 5 (𝑦 ∈ ω ↔ 𝑦 ω)
41 peano2 4593 . . . . . 6 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
4241adantl 277 . . . . 5 ((𝜑𝑦 ∈ ω) → suc 𝑦 ∈ ω)
4340, 42sylan2br 288 . . . 4 ((𝜑𝑦 ω) → suc 𝑦 ∈ ω)
446, 39eleqtrdi 2270 . . . 4 (𝜑𝐵 ω)
452, 10, 12, 36, 43, 44tfrcl 6362 . . 3 (𝜑 → (𝐺𝐵) ∈ 𝑆)
468, 45eqeltrd 2254 . 2 (𝜑 → ((𝐺 ↾ ω)‘𝐵) ∈ 𝑆)
475, 46eqeltrid 2264 1 (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wo 708  w3a 978   = wceq 1353  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2737  c0 3422   cuni 3809  cmpt 4063  Ord word 4361  Lim wlim 4363  suc csuc 4364  ωcom 4588  dom cdm 4625  cres 4627  Fun wfun 5209  wf 5211  cfv 5215  recscrecs 6302  freccfrec 6388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4117  ax-sep 4120  ax-nul 4128  ax-pow 4173  ax-pr 4208  ax-un 4432  ax-setind 4535  ax-iinf 4586
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4003  df-opab 4064  df-mpt 4065  df-tr 4101  df-id 4292  df-iord 4365  df-on 4367  df-ilim 4368  df-suc 4370  df-iom 4589  df-xp 4631  df-rel 4632  df-cnv 4633  df-co 4634  df-dm 4635  df-rn 4636  df-res 4637  df-ima 4638  df-iota 5177  df-fun 5217  df-fn 5218  df-f 5219  df-f1 5220  df-fo 5221  df-f1o 5222  df-fv 5223  df-recs 6303  df-frec 6389
This theorem is referenced by:  freccl  6401
  Copyright terms: Public domain W3C validator