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

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

Proof of Theorem tfr1onlemubacc
StepHypRef Expression
1 tfr1on.f . . . . . . . . 9 𝐹 = recs(𝐺)
2 tfr1on.g . . . . . . . . 9 (𝜑 → Fun 𝐺)
3 tfr1on.x . . . . . . . . 9 (𝜑 → Ord 𝑋)
4 tfr1on.ex . . . . . . . . 9 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
5 tfr1onlemsucfn.1 . . . . . . . . 9 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6 tfr1onlembacc.3 . . . . . . . . 9 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7 tfr1onlembacc.u . . . . . . . . 9 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
8 tfr1onlembacc.4 . . . . . . . . 9 (𝜑𝐷𝑋)
9 tfr1onlembacc.5 . . . . . . . . 9 (𝜑 → ∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
101, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembfn 6348 . . . . . . . 8 (𝜑 𝐵 Fn 𝐷)
11 fndm 5317 . . . . . . . 8 ( 𝐵 Fn 𝐷 → dom 𝐵 = 𝐷)
1210, 11syl 14 . . . . . . 7 (𝜑 → dom 𝐵 = 𝐷)
131, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembacc 6346 . . . . . . . . . 10 (𝜑𝐵𝐴)
1413unissd 3835 . . . . . . . . 9 (𝜑 𝐵 𝐴)
155, 3tfr1onlemssrecs 6343 . . . . . . . . 9 (𝜑 𝐴 ⊆ recs(𝐺))
1614, 15sstrd 3167 . . . . . . . 8 (𝜑 𝐵 ⊆ recs(𝐺))
17 dmss 4828 . . . . . . . 8 ( 𝐵 ⊆ recs(𝐺) → dom 𝐵 ⊆ dom recs(𝐺))
1816, 17syl 14 . . . . . . 7 (𝜑 → dom 𝐵 ⊆ dom recs(𝐺))
1912, 18eqsstrrd 3194 . . . . . 6 (𝜑𝐷 ⊆ dom recs(𝐺))
2019sselda 3157 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ dom recs(𝐺))
21 eqid 2177 . . . . . 6 {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
2221tfrlem9 6323 . . . . 5 (𝑤 ∈ dom recs(𝐺) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤)))
2320, 22syl 14 . . . 4 ((𝜑𝑤𝐷) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤)))
24 tfrfun 6324 . . . . 5 Fun recs(𝐺)
2512eleq2d 2247 . . . . . 6 (𝜑 → (𝑤 ∈ dom 𝐵𝑤𝐷))
2625biimpar 297 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ dom 𝐵)
27 funssfv 5543 . . . . 5 ((Fun recs(𝐺) ∧ 𝐵 ⊆ recs(𝐺) ∧ 𝑤 ∈ dom 𝐵) → (recs(𝐺)‘𝑤) = ( 𝐵𝑤))
2824, 16, 26, 27mp3an2ani 1344 . . . 4 ((𝜑𝑤𝐷) → (recs(𝐺)‘𝑤) = ( 𝐵𝑤))
29 ordelon 4385 . . . . . . . . . 10 ((Ord 𝑋𝐷𝑋) → 𝐷 ∈ On)
303, 8, 29syl2anc 411 . . . . . . . . 9 (𝜑𝐷 ∈ On)
31 eloni 4377 . . . . . . . . 9 (𝐷 ∈ On → Ord 𝐷)
3230, 31syl 14 . . . . . . . 8 (𝜑 → Ord 𝐷)
33 ordelss 4381 . . . . . . . 8 ((Ord 𝐷𝑤𝐷) → 𝑤𝐷)
3432, 33sylan 283 . . . . . . 7 ((𝜑𝑤𝐷) → 𝑤𝐷)
3512adantr 276 . . . . . . 7 ((𝜑𝑤𝐷) → dom 𝐵 = 𝐷)
3634, 35sseqtrrd 3196 . . . . . 6 ((𝜑𝑤𝐷) → 𝑤 ⊆ dom 𝐵)
37 fun2ssres 5261 . . . . . 6 ((Fun recs(𝐺) ∧ 𝐵 ⊆ recs(𝐺) ∧ 𝑤 ⊆ dom 𝐵) → (recs(𝐺) ↾ 𝑤) = ( 𝐵𝑤))
3824, 16, 36, 37mp3an2ani 1344 . . . . 5 ((𝜑𝑤𝐷) → (recs(𝐺) ↾ 𝑤) = ( 𝐵𝑤))
3938fveq2d 5521 . . . 4 ((𝜑𝑤𝐷) → (𝐺‘(recs(𝐺) ↾ 𝑤)) = (𝐺‘( 𝐵𝑤)))
4023, 28, 393eqtr3d 2218 . . 3 ((𝜑𝑤𝐷) → ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
4140ralrimiva 2550 . 2 (𝜑 → ∀𝑤𝐷 ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
42 fveq2 5517 . . . 4 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
43 reseq2 4904 . . . . 5 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
4443fveq2d 5521 . . . 4 (𝑢 = 𝑤 → (𝐺‘( 𝐵𝑢)) = (𝐺‘( 𝐵𝑤)))
4542, 44eqeq12d 2192 . . 3 (𝑢 = 𝑤 → (( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)) ↔ ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤))))
4645cbvralv 2705 . 2 (∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)) ↔ ∀𝑤𝐷 ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
4741, 46sylibr 134 1 (𝜑 → ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978   = wceq 1353  wex 1492  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2739  cun 3129  wss 3131  {csn 3594  cop 3597   cuni 3811  Ord word 4364  Oncon0 4365  suc csuc 4367  dom cdm 4628  cres 4630  Fun wfun 5212   Fn wfn 5213  cfv 5218  recscrecs 6308
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-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
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-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-fv 5226  df-recs 6309
This theorem is referenced by:  tfr1onlemex  6351
  Copyright terms: Public domain W3C validator