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

Theorem tfrlemiubacc 5974
Description: The union of 𝐵 satisfies the recursion rule (lemma for tfrlemi1 5976). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
Hypotheses
Ref Expression
tfrlemisucfn.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
tfrlemisucfn.2 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
tfrlemi1.3 𝐵 = { ∣ ∃𝑧𝑥𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))}
tfrlemi1.4 (𝜑𝑥 ∈ On)
tfrlemi1.5 (𝜑 → ∀𝑧𝑥𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
Assertion
Ref Expression
tfrlemiubacc (𝜑 → ∀𝑢𝑥 ( 𝐵𝑢) = (𝐹‘( 𝐵𝑢)))
Distinct variable groups:   𝑓,𝑔,,𝑢,𝑤,𝑥,𝑦,𝑧,𝐴   𝑓,𝐹,𝑔,,𝑢,𝑤,𝑥,𝑦,𝑧   𝜑,𝑤,𝑦   𝑢,𝐵,𝑤,𝑓,𝑔,,𝑧   𝜑,𝑔,,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑢,𝑓)   𝐵(𝑥,𝑦)

Proof of Theorem tfrlemiubacc
StepHypRef Expression
1 tfrlemisucfn.1 . . . . . . . . 9 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
2 tfrlemisucfn.2 . . . . . . . . 9 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
3 tfrlemi1.3 . . . . . . . . 9 𝐵 = { ∣ ∃𝑧𝑥𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}))}
4 tfrlemi1.4 . . . . . . . . 9 (𝜑𝑥 ∈ On)
5 tfrlemi1.5 . . . . . . . . 9 (𝜑 → ∀𝑧𝑥𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐹‘(𝑔𝑤))))
61, 2, 3, 4, 5tfrlemibfn 5972 . . . . . . . 8 (𝜑 𝐵 Fn 𝑥)
7 fndm 5025 . . . . . . . 8 ( 𝐵 Fn 𝑥 → dom 𝐵 = 𝑥)
86, 7syl 14 . . . . . . 7 (𝜑 → dom 𝐵 = 𝑥)
91, 2, 3, 4, 5tfrlemibacc 5970 . . . . . . . . . 10 (𝜑𝐵𝐴)
109unissd 3631 . . . . . . . . 9 (𝜑 𝐵 𝐴)
111recsfval 5961 . . . . . . . . 9 recs(𝐹) = 𝐴
1210, 11syl6sseqr 3019 . . . . . . . 8 (𝜑 𝐵 ⊆ recs(𝐹))
13 dmss 4561 . . . . . . . 8 ( 𝐵 ⊆ recs(𝐹) → dom 𝐵 ⊆ dom recs(𝐹))
1412, 13syl 14 . . . . . . 7 (𝜑 → dom 𝐵 ⊆ dom recs(𝐹))
158, 14eqsstr3d 3007 . . . . . 6 (𝜑𝑥 ⊆ dom recs(𝐹))
1615sselda 2972 . . . . 5 ((𝜑𝑤𝑥) → 𝑤 ∈ dom recs(𝐹))
171tfrlem9 5965 . . . . 5 (𝑤 ∈ dom recs(𝐹) → (recs(𝐹)‘𝑤) = (𝐹‘(recs(𝐹) ↾ 𝑤)))
1816, 17syl 14 . . . 4 ((𝜑𝑤𝑥) → (recs(𝐹)‘𝑤) = (𝐹‘(recs(𝐹) ↾ 𝑤)))
191tfrlem7 5963 . . . . . 6 Fun recs(𝐹)
2019a1i 9 . . . . 5 ((𝜑𝑤𝑥) → Fun recs(𝐹))
2112adantr 265 . . . . 5 ((𝜑𝑤𝑥) → 𝐵 ⊆ recs(𝐹))
228eleq2d 2123 . . . . . 6 (𝜑 → (𝑤 ∈ dom 𝐵𝑤𝑥))
2322biimpar 285 . . . . 5 ((𝜑𝑤𝑥) → 𝑤 ∈ dom 𝐵)
24 funssfv 5226 . . . . 5 ((Fun recs(𝐹) ∧ 𝐵 ⊆ recs(𝐹) ∧ 𝑤 ∈ dom 𝐵) → (recs(𝐹)‘𝑤) = ( 𝐵𝑤))
2520, 21, 23, 24syl3anc 1146 . . . 4 ((𝜑𝑤𝑥) → (recs(𝐹)‘𝑤) = ( 𝐵𝑤))
26 eloni 4139 . . . . . . . . 9 (𝑥 ∈ On → Ord 𝑥)
274, 26syl 14 . . . . . . . 8 (𝜑 → Ord 𝑥)
28 ordelss 4143 . . . . . . . 8 ((Ord 𝑥𝑤𝑥) → 𝑤𝑥)
2927, 28sylan 271 . . . . . . 7 ((𝜑𝑤𝑥) → 𝑤𝑥)
308adantr 265 . . . . . . 7 ((𝜑𝑤𝑥) → dom 𝐵 = 𝑥)
3129, 30sseqtr4d 3009 . . . . . 6 ((𝜑𝑤𝑥) → 𝑤 ⊆ dom 𝐵)
32 fun2ssres 4970 . . . . . 6 ((Fun recs(𝐹) ∧ 𝐵 ⊆ recs(𝐹) ∧ 𝑤 ⊆ dom 𝐵) → (recs(𝐹) ↾ 𝑤) = ( 𝐵𝑤))
3320, 21, 31, 32syl3anc 1146 . . . . 5 ((𝜑𝑤𝑥) → (recs(𝐹) ↾ 𝑤) = ( 𝐵𝑤))
3433fveq2d 5209 . . . 4 ((𝜑𝑤𝑥) → (𝐹‘(recs(𝐹) ↾ 𝑤)) = (𝐹‘( 𝐵𝑤)))
3518, 25, 343eqtr3d 2096 . . 3 ((𝜑𝑤𝑥) → ( 𝐵𝑤) = (𝐹‘( 𝐵𝑤)))
3635ralrimiva 2409 . 2 (𝜑 → ∀𝑤𝑥 ( 𝐵𝑤) = (𝐹‘( 𝐵𝑤)))
37 fveq2 5205 . . . 4 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
38 reseq2 4634 . . . . 5 (𝑢 = 𝑤 → ( 𝐵𝑢) = ( 𝐵𝑤))
3938fveq2d 5209 . . . 4 (𝑢 = 𝑤 → (𝐹‘( 𝐵𝑢)) = (𝐹‘( 𝐵𝑤)))
4037, 39eqeq12d 2070 . . 3 (𝑢 = 𝑤 → (( 𝐵𝑢) = (𝐹‘( 𝐵𝑢)) ↔ ( 𝐵𝑤) = (𝐹‘( 𝐵𝑤))))
4140cbvralv 2550 . 2 (∀𝑢𝑥 ( 𝐵𝑢) = (𝐹‘( 𝐵𝑢)) ↔ ∀𝑤𝑥 ( 𝐵𝑤) = (𝐹‘( 𝐵𝑤)))
4236, 41sylibr 141 1 (𝜑 → ∀𝑢𝑥 ( 𝐵𝑢) = (𝐹‘( 𝐵𝑢)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896  wal 1257   = wceq 1259  wex 1397  wcel 1409  {cab 2042  wral 2323  wrex 2324  Vcvv 2574  cun 2942  wss 2944  {csn 3402  cop 3405   cuni 3607  Ord word 4126  Oncon0 4127  dom cdm 4372  cres 4374  Fun wfun 4923   Fn wfn 4924  cfv 4929  recscrecs 5949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-fv 4937  df-recs 5950
This theorem is referenced by:  tfrlemiex  5975
  Copyright terms: Public domain W3C validator