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

Theorem tfrcllemubacc 6080
Description: Lemma for tfrcl 6085. The union of 𝐵 satisfies the recursion rule. (Contributed by Jim Kingdon, 25-Mar-2022.)
Hypotheses
Ref Expression
tfrcl.f 𝐹 = recs(𝐺)
tfrcl.g (𝜑 → Fun 𝐺)
tfrcl.x (𝜑 → Ord 𝑋)
tfrcl.ex ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
tfrcllemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfrcllembacc.3 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
tfrcllembacc.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfrcllembacc.4 (𝜑𝐷𝑋)
tfrcllembacc.5 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
Assertion
Ref Expression
tfrcllemubacc (𝜑 → ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)))
Distinct variable groups:   𝐴,𝑓,𝑔,,𝑥,𝑦,𝑧   𝐷,𝑓,𝑔,𝑥,𝑦   𝑓,𝐺,𝑥,𝑦   𝑆,𝑓,𝑥,𝑦   𝑓,𝑋,𝑥   𝜑,𝑓,𝑔,,𝑥,𝑦,𝑧   𝐵,𝑔,,𝑧   𝑢,𝐵,𝑤   𝐷,,𝑧   𝑢,𝐷,𝑤   𝑤,𝐺   ,𝐺,𝑧   𝑢,𝐺   𝑆,𝑔,,𝑧   𝑧,𝑋   𝑤,𝑔,𝜑,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑢)   𝐴(𝑤,𝑢)   𝐵(𝑥,𝑦,𝑓)   𝑆(𝑤,𝑢)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑢,𝑓,𝑔,)   𝐺(𝑔)   𝑋(𝑦,𝑤,𝑢,𝑔,)

Proof of Theorem tfrcllemubacc
Dummy variables 𝑒 𝑡 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrcl.f . . . . . . . . 9 𝐹 = recs(𝐺)
2 tfrcl.g . . . . . . . . 9 (𝜑 → Fun 𝐺)
3 tfrcl.x . . . . . . . . 9 (𝜑 → Ord 𝑋)
4 tfrcl.ex . . . . . . . . 9 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
5 tfrcllemsucfn.1 . . . . . . . . 9 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6 tfrcllembacc.3 . . . . . . . . 9 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7 tfrcllembacc.u . . . . . . . . 9 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
8 tfrcllembacc.4 . . . . . . . . 9 (𝜑𝐷𝑋)
9 tfrcllembacc.5 . . . . . . . . 9 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
101, 2, 3, 4, 5, 6, 7, 8, 9tfrcllembfn 6078 . . . . . . . 8 (𝜑 𝐵:𝐷𝑆)
11 fdm 5133 . . . . . . . 8 ( 𝐵:𝐷𝑆 → dom 𝐵 = 𝐷)
1210, 11syl 14 . . . . . . 7 (𝜑 → dom 𝐵 = 𝐷)
131, 2, 3, 4, 5, 6, 7, 8, 9tfrcllembacc 6076 . . . . . . . . . 10 (𝜑𝐵𝐴)
1413unissd 3662 . . . . . . . . 9 (𝜑 𝐵 𝐴)
155, 3tfrcllemssrecs 6073 . . . . . . . . 9 (𝜑 𝐴 ⊆ recs(𝐺))
1614, 15sstrd 3024 . . . . . . . 8 (𝜑 𝐵 ⊆ recs(𝐺))
17 dmss 4605 . . . . . . . 8 ( 𝐵 ⊆ recs(𝐺) → dom 𝐵 ⊆ dom recs(𝐺))
1816, 17syl 14 . . . . . . 7 (𝜑 → dom 𝐵 ⊆ dom recs(𝐺))
1912, 18eqsstr3d 3050 . . . . . 6 (𝜑𝐷 ⊆ dom recs(𝐺))
2019sselda 3014 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ dom recs(𝐺))
21 eqid 2085 . . . . . 6 {𝑒 ∣ ∃𝑣 ∈ On (𝑒 Fn 𝑣 ∧ ∀𝑡𝑣 (𝑒𝑡) = (𝐺‘(𝑒𝑡)))} = {𝑒 ∣ ∃𝑣 ∈ On (𝑒 Fn 𝑣 ∧ ∀𝑡𝑣 (𝑒𝑡) = (𝐺‘(𝑒𝑡)))}
2221tfrlem9 6040 . . . . 5 (𝑤 ∈ dom recs(𝐺) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤)))
2320, 22syl 14 . . . 4 ((𝜑𝑤𝐷) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤)))
24 tfrfun 6041 . . . . 5 Fun recs(𝐺)
2512eleq2d 2154 . . . . . 6 (𝜑 → (𝑤 ∈ dom 𝐵𝑤𝐷))
2625biimpar 291 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ dom 𝐵)
27 funssfv 5295 . . . . 5 ((Fun recs(𝐺) ∧ 𝐵 ⊆ recs(𝐺) ∧ 𝑤 ∈ dom 𝐵) → (recs(𝐺)‘𝑤) = ( 𝐵𝑤))
2824, 16, 26, 27mp3an2ani 1278 . . . 4 ((𝜑𝑤𝐷) → (recs(𝐺)‘𝑤) = ( 𝐵𝑤))
29 ordelon 4186 . . . . . . . . . 10 ((Ord 𝑋𝐷𝑋) → 𝐷 ∈ On)
303, 8, 29syl2anc 403 . . . . . . . . 9 (𝜑𝐷 ∈ On)
31 eloni 4178 . . . . . . . . 9 (𝐷 ∈ On → Ord 𝐷)
3230, 31syl 14 . . . . . . . 8 (𝜑 → Ord 𝐷)
33 ordelss 4182 . . . . . . . 8 ((Ord 𝐷𝑤𝐷) → 𝑤𝐷)
3432, 33sylan 277 . . . . . . 7 ((𝜑𝑤𝐷) → 𝑤𝐷)
3512adantr 270 . . . . . . 7 ((𝜑𝑤𝐷) → dom 𝐵 = 𝐷)
3634, 35sseqtr4d 3052 . . . . . 6 ((𝜑𝑤𝐷) → 𝑤 ⊆ dom 𝐵)
37 fun2ssres 5024 . . . . . 6 ((Fun recs(𝐺) ∧ 𝐵 ⊆ recs(𝐺) ∧ 𝑤 ⊆ dom 𝐵) → (recs(𝐺) ↾ 𝑤) = ( 𝐵𝑤))
3824, 16, 36, 37mp3an2ani 1278 . . . . 5 ((𝜑𝑤𝐷) → (recs(𝐺) ↾ 𝑤) = ( 𝐵𝑤))
3938fveq2d 5274 . . . 4 ((𝜑𝑤𝐷) → (𝐺‘(recs(𝐺) ↾ 𝑤)) = (𝐺‘( 𝐵𝑤)))
4023, 28, 393eqtr3d 2125 . . 3 ((𝜑𝑤𝐷) → ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
4140ralrimiva 2442 . 2 (𝜑 → ∀𝑤𝐷 ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
42 fveq2 5270 . . . 4 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
43 reseq2 4678 . . . . 5 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
4443fveq2d 5274 . . . 4 (𝑢 = 𝑤 → (𝐺‘( 𝐵𝑢)) = (𝐺‘( 𝐵𝑤)))
4542, 44eqeq12d 2099 . . 3 (𝑢 = 𝑤 → (( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)) ↔ ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤))))
4645cbvralv 2586 . 2 (∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)) ↔ ∀𝑤𝐷 ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
4741, 46sylibr 132 1 (𝜑 → ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922   = wceq 1287  wex 1424  wcel 1436  {cab 2071  wral 2355  wrex 2356  cun 2986  wss 2988  {csn 3431  cop 3434   cuni 3638  Ord word 4165  Oncon0 4166  suc csuc 4168  dom cdm 4413  cres 4415  Fun wfun 4977   Fn wfn 4978  wf 4979  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-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-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-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:  tfrcllemex  6081
  Copyright terms: Public domain W3C validator