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

Theorem tfr1onlemubacc 6209
Description: Lemma for tfr1on 6213. 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 6207 . . . . . . . 8 (𝜑 𝐵 Fn 𝐷)
11 fndm 5190 . . . . . . . 8 ( 𝐵 Fn 𝐷 → dom 𝐵 = 𝐷)
1210, 11syl 14 . . . . . . 7 (𝜑 → dom 𝐵 = 𝐷)
131, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembacc 6205 . . . . . . . . . 10 (𝜑𝐵𝐴)
1413unissd 3728 . . . . . . . . 9 (𝜑 𝐵 𝐴)
155, 3tfr1onlemssrecs 6202 . . . . . . . . 9 (𝜑 𝐴 ⊆ recs(𝐺))
1614, 15sstrd 3075 . . . . . . . 8 (𝜑 𝐵 ⊆ recs(𝐺))
17 dmss 4706 . . . . . . . 8 ( 𝐵 ⊆ recs(𝐺) → dom 𝐵 ⊆ dom recs(𝐺))
1816, 17syl 14 . . . . . . 7 (𝜑 → dom 𝐵 ⊆ dom recs(𝐺))
1912, 18eqsstrrd 3102 . . . . . 6 (𝜑𝐷 ⊆ dom recs(𝐺))
2019sselda 3065 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ dom recs(𝐺))
21 eqid 2115 . . . . . 6 {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
2221tfrlem9 6182 . . . . 5 (𝑤 ∈ dom recs(𝐺) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤)))
2320, 22syl 14 . . . 4 ((𝜑𝑤𝐷) → (recs(𝐺)‘𝑤) = (𝐺‘(recs(𝐺) ↾ 𝑤)))
24 tfrfun 6183 . . . . 5 Fun recs(𝐺)
2512eleq2d 2185 . . . . . 6 (𝜑 → (𝑤 ∈ dom 𝐵𝑤𝐷))
2625biimpar 293 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ dom 𝐵)
27 funssfv 5413 . . . . 5 ((Fun recs(𝐺) ∧ 𝐵 ⊆ recs(𝐺) ∧ 𝑤 ∈ dom 𝐵) → (recs(𝐺)‘𝑤) = ( 𝐵𝑤))
2824, 16, 26, 27mp3an2ani 1305 . . . 4 ((𝜑𝑤𝐷) → (recs(𝐺)‘𝑤) = ( 𝐵𝑤))
29 ordelon 4273 . . . . . . . . . 10 ((Ord 𝑋𝐷𝑋) → 𝐷 ∈ On)
303, 8, 29syl2anc 406 . . . . . . . . 9 (𝜑𝐷 ∈ On)
31 eloni 4265 . . . . . . . . 9 (𝐷 ∈ On → Ord 𝐷)
3230, 31syl 14 . . . . . . . 8 (𝜑 → Ord 𝐷)
33 ordelss 4269 . . . . . . . 8 ((Ord 𝐷𝑤𝐷) → 𝑤𝐷)
3432, 33sylan 279 . . . . . . 7 ((𝜑𝑤𝐷) → 𝑤𝐷)
3512adantr 272 . . . . . . 7 ((𝜑𝑤𝐷) → dom 𝐵 = 𝐷)
3634, 35sseqtrrd 3104 . . . . . 6 ((𝜑𝑤𝐷) → 𝑤 ⊆ dom 𝐵)
37 fun2ssres 5134 . . . . . 6 ((Fun recs(𝐺) ∧ 𝐵 ⊆ recs(𝐺) ∧ 𝑤 ⊆ dom 𝐵) → (recs(𝐺) ↾ 𝑤) = ( 𝐵𝑤))
3824, 16, 36, 37mp3an2ani 1305 . . . . 5 ((𝜑𝑤𝐷) → (recs(𝐺) ↾ 𝑤) = ( 𝐵𝑤))
3938fveq2d 5391 . . . 4 ((𝜑𝑤𝐷) → (𝐺‘(recs(𝐺) ↾ 𝑤)) = (𝐺‘( 𝐵𝑤)))
4023, 28, 393eqtr3d 2156 . . 3 ((𝜑𝑤𝐷) → ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
4140ralrimiva 2480 . 2 (𝜑 → ∀𝑤𝐷 ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
42 fveq2 5387 . . . 4 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
43 reseq2 4782 . . . . 5 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
4443fveq2d 5391 . . . 4 (𝑢 = 𝑤 → (𝐺‘( 𝐵𝑢)) = (𝐺‘( 𝐵𝑤)))
4542, 44eqeq12d 2130 . . 3 (𝑢 = 𝑤 → (( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)) ↔ ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤))))
4645cbvralv 2629 . 2 (∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)) ↔ ∀𝑤𝐷 ( 𝐵𝑤) = (𝐺‘( 𝐵𝑤)))
4741, 46sylibr 133 1 (𝜑 → ∀𝑢𝐷 ( 𝐵𝑢) = (𝐺‘( 𝐵𝑢)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945   = wceq 1314  wex 1451  wcel 1463  {cab 2101  wral 2391  wrex 2392  Vcvv 2658  cun 3037  wss 3039  {csn 3495  cop 3498   cuni 3704  Ord word 4252  Oncon0 4253  suc csuc 4255  dom cdm 4507  cres 4509  Fun wfun 5085   Fn wfn 5086  cfv 5091  recscrecs 6167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-suc 4261  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099  df-recs 6168
This theorem is referenced by:  tfr1onlemex  6210
  Copyright terms: Public domain W3C validator