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

Theorem freceq1 6295
Description: Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
Assertion
Ref Expression
freceq1 (𝐹 = 𝐺 → frec(𝐹, 𝐴) = frec(𝐺, 𝐴))

Proof of Theorem freceq1
Dummy variables 𝑥 𝑔 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 108 . . . . . . . . . . 11 ((𝐹 = 𝐺𝑔 ∈ V) → 𝐹 = 𝐺)
21fveq1d 5429 . . . . . . . . . 10 ((𝐹 = 𝐺𝑔 ∈ V) → (𝐹‘(𝑔𝑚)) = (𝐺‘(𝑔𝑚)))
32eleq2d 2210 . . . . . . . . 9 ((𝐹 = 𝐺𝑔 ∈ V) → (𝑥 ∈ (𝐹‘(𝑔𝑚)) ↔ 𝑥 ∈ (𝐺‘(𝑔𝑚))))
43anbi2d 460 . . . . . . . 8 ((𝐹 = 𝐺𝑔 ∈ V) → ((dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚)))))
54rexbidv 2439 . . . . . . 7 ((𝐹 = 𝐺𝑔 ∈ V) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚)))))
65orbi1d 781 . . . . . 6 ((𝐹 = 𝐺𝑔 ∈ V) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))))
76abbidv 2258 . . . . 5 ((𝐹 = 𝐺𝑔 ∈ V) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})
87mpteq2dva 4024 . . . 4 (𝐹 = 𝐺 → (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}))
9 recseq 6209 . . . 4 ((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))}) → recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
108, 9syl 14 . . 3 (𝐹 = 𝐺 → recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})))
1110reseq1d 4824 . 2 (𝐹 = 𝐺 → (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω))
12 df-frec 6294 . 2 frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐹‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
13 df-frec 6294 . 2 frec(𝐺, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚𝑥 ∈ (𝐺‘(𝑔𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥𝐴))})) ↾ ω)
1411, 12, 133eqtr4g 2198 1 (𝐹 = 𝐺 → frec(𝐹, 𝐴) = frec(𝐺, 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 698   = wceq 1332  wcel 1481  {cab 2126  wrex 2418  Vcvv 2689  c0 3366  cmpt 3995  suc csuc 4293  ωcom 4510  dom cdm 4545  cres 4547  cfv 5129  recscrecs 6207  freccfrec 6293
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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-in 3080  df-uni 3743  df-br 3936  df-opab 3996  df-mpt 3997  df-res 4557  df-iota 5094  df-fv 5137  df-recs 6208  df-frec 6294
This theorem is referenced by:  frecuzrdgdom  10220  frecuzrdgfun  10222  frecuzrdgsuct  10226  seqeq1  10250  seqeq2  10251  seqeq3  10252  iseqvalcbv  10259  hashfz1  10559  ennnfonelemr  11965  ctinfom  11970  isomninn  13394  iswomninn  13411  ismkvnn  13413
  Copyright terms: Public domain W3C validator