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

Theorem frecrdg 5970
Description: Transfinite recursion restricted to omega.

Given a suitable characteristic function, df-frec 5956 produces the same results as df-irdg 5935 restricted to ω.

Presumably the theorem would also hold if 𝐹 Fn V were changed to 𝑧(𝐹𝑧) ∈ V. (Contributed by Jim Kingdon, 29-Aug-2019.)

Hypotheses
Ref Expression
frecrdg.1 (𝜑𝐹 Fn V)
frecrdg.2 (𝜑𝐴𝑉)
frecrdg.inc (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹𝑥))
Assertion
Ref Expression
frecrdg (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝑉   𝜑,𝑥

Proof of Theorem frecrdg
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frecrdg.1 . . . 4 (𝜑𝐹 Fn V)
2 vex 2557 . . . . . 6 𝑧 ∈ V
3 funfvex 5170 . . . . . . 7 ((Fun 𝐹𝑧 ∈ dom 𝐹) → (𝐹𝑧) ∈ V)
43funfni 4977 . . . . . 6 ((𝐹 Fn V ∧ 𝑧 ∈ V) → (𝐹𝑧) ∈ V)
52, 4mpan2 401 . . . . 5 (𝐹 Fn V → (𝐹𝑧) ∈ V)
65alrimiv 1754 . . . 4 (𝐹 Fn V → ∀𝑧(𝐹𝑧) ∈ V)
71, 6syl 14 . . 3 (𝜑 → ∀𝑧(𝐹𝑧) ∈ V)
8 frecrdg.2 . . 3 (𝜑𝐴𝑉)
9 frecfnom 5964 . . 3 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉) → frec(𝐹, 𝐴) Fn ω)
107, 8, 9syl2anc 391 . 2 (𝜑 → frec(𝐹, 𝐴) Fn ω)
11 rdgifnon2 5945 . . . 4 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉) → rec(𝐹, 𝐴) Fn On)
127, 8, 11syl2anc 391 . . 3 (𝜑 → rec(𝐹, 𝐴) Fn On)
13 omsson 4313 . . 3 ω ⊆ On
14 fnssres 4990 . . 3 ((rec(𝐹, 𝐴) Fn On ∧ ω ⊆ On) → (rec(𝐹, 𝐴) ↾ ω) Fn ω)
1512, 13, 14sylancl 392 . 2 (𝜑 → (rec(𝐹, 𝐴) ↾ ω) Fn ω)
16 fveq2 5156 . . . . 5 (𝑥 = ∅ → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘∅))
17 fveq2 5156 . . . . 5 (𝑥 = ∅ → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘∅))
1816, 17eqeq12d 2054 . . . 4 (𝑥 = ∅ → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾ ω)‘∅)))
19 fveq2 5156 . . . . 5 (𝑥 = 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘𝑦))
20 fveq2 5156 . . . . 5 (𝑥 = 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦))
2119, 20eqeq12d 2054 . . . 4 (𝑥 = 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)))
22 fveq2 5156 . . . . 5 (𝑥 = suc 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘suc 𝑦))
23 fveq2 5156 . . . . 5 (𝑥 = suc 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))
2422, 23eqeq12d 2054 . . . 4 (𝑥 = suc 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)))
25 frec0g 5961 . . . . . 6 (𝐴𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴)
268, 25syl 14 . . . . 5 (𝜑 → (frec(𝐹, 𝐴)‘∅) = 𝐴)
27 peano1 4295 . . . . . . 7 ∅ ∈ ω
28 fvres 5176 . . . . . . 7 (∅ ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = (rec(𝐹, 𝐴)‘∅))
2927, 28ax-mp 7 . . . . . 6 ((rec(𝐹, 𝐴) ↾ ω)‘∅) = (rec(𝐹, 𝐴)‘∅)
30 rdg0g 5953 . . . . . . 7 (𝐴𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
318, 30syl 14 . . . . . 6 (𝜑 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
3229, 31syl5eq 2084 . . . . 5 (𝜑 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴)
3326, 32eqtr4d 2075 . . . 4 (𝜑 → (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾ ω)‘∅))
34 simpr 103 . . . . . . . . . 10 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦))
35 fvres 5176 . . . . . . . . . . 11 (𝑦 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦))
3635ad2antlr 458 . . . . . . . . . 10 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦))
3734, 36eqtrd 2072 . . . . . . . . 9 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦))
3837fveq2d 5160 . . . . . . . 8 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦)))
397, 8jca 290 . . . . . . . . . 10 (𝜑 → (∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉))
40 frecsuc 5969 . . . . . . . . . . 11 ((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
41403expa 1104 . . . . . . . . . 10 (((∀𝑧(𝐹𝑧) ∈ V ∧ 𝐴𝑉) ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
4239, 41sylan 267 . . . . . . . . 9 ((𝜑𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
4342adantr 261 . . . . . . . 8 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
441adantr 261 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω) → 𝐹 Fn V)
458adantr 261 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω) → 𝐴𝑉)
46 simpr 103 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ω) → 𝑦 ∈ ω)
47 nnon 4310 . . . . . . . . . . 11 (𝑦 ∈ ω → 𝑦 ∈ On)
4846, 47syl 14 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω) → 𝑦 ∈ On)
49 frecrdg.inc . . . . . . . . . . 11 (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹𝑥))
5049adantr 261 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω) → ∀𝑥 𝑥 ⊆ (𝐹𝑥))
5144, 45, 48, 50rdgisucinc 5950 . . . . . . . . 9 ((𝜑𝑦 ∈ ω) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦)))
5251adantr 261 . . . . . . . 8 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦)))
5338, 43, 523eqtr4d 2082 . . . . . . 7 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
54 peano2 4296 . . . . . . . . 9 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
55 fvres 5176 . . . . . . . . 9 (suc 𝑦 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
5654, 55syl 14 . . . . . . . 8 (𝑦 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
5756ad2antlr 458 . . . . . . 7 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
5853, 57eqtr4d 2075 . . . . . 6 (((𝜑𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))
5958ex 108 . . . . 5 ((𝜑𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)))
6059expcom 109 . . . 4 (𝑦 ∈ ω → (𝜑 → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))))
6118, 21, 24, 33, 60finds2 4302 . . 3 (𝑥 ∈ ω → (𝜑 → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥)))
6261impcom 116 . 2 ((𝜑𝑥 ∈ ω) → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥))
6310, 15, 62eqfnfvd 5246 1 (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wal 1241   = wceq 1243  wcel 1393  Vcvv 2554  wss 2914  c0 3221  Oncon0 4087  suc csuc 4089  ωcom 4291  cres 4325   Fn wfn 4875  cfv 4880  reccrdg 5934  freccfrec 5955
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3869  ax-sep 3872  ax-nul 3880  ax-pow 3924  ax-pr 3941  ax-un 4157  ax-setind 4247  ax-iinf 4289
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2308  df-rex 2309  df-reu 2310  df-rab 2312  df-v 2556  df-sbc 2762  df-csb 2850  df-dif 2917  df-un 2919  df-in 2921  df-ss 2928  df-nul 3222  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-int 3613  df-iun 3656  df-br 3762  df-opab 3816  df-mpt 3817  df-tr 3852  df-id 4027  df-iord 4090  df-on 4092  df-suc 4095  df-iom 4292  df-xp 4329  df-rel 4330  df-cnv 4331  df-co 4332  df-dm 4333  df-rn 4334  df-res 4335  df-ima 4336  df-iota 4845  df-fun 4882  df-fn 4883  df-f 4884  df-f1 4885  df-fo 4886  df-f1o 4887  df-fv 4888  df-recs 5898  df-irdg 5935  df-frec 5956
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator