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.

Step	Hyp	Ref	Expression
1		frecrdg.1	. . . 4 ⊢ (𝜑 → 𝐹 Fn V)
2		vex 2557	. . . . . 6 ⊢ 𝑧 ∈ V
3		funfvex 5170	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ V)
4	3	funfni 4977	. . . . . 6 ⊢ ((𝐹 Fn V ∧ 𝑧 ∈ V) → (𝐹‘𝑧) ∈ V)
5	2, 4	mpan2 401	. . . . 5 ⊢ (𝐹 Fn V → (𝐹‘𝑧) ∈ V)
6	5	alrimiv 1754	. . . 4 ⊢ (𝐹 Fn V → ∀𝑧(𝐹‘𝑧) ∈ V)
7	1, 6	syl 14	. . 3 ⊢ (𝜑 → ∀𝑧(𝐹‘𝑧) ∈ V)
8		frecrdg.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
9		frecfnom 5964	. . 3 ⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → frec(𝐹, 𝐴) Fn ω)
10	7, 8, 9	syl2anc 391	. 2 ⊢ (𝜑 → frec(𝐹, 𝐴) Fn ω)
11		rdgifnon2 5945	. . . 4 ⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On)
12	7, 8, 11	syl2anc 391	. . 3 ⊢ (𝜑 → rec(𝐹, 𝐴) Fn On)
13		omsson 4313	. . 3 ⊢ ω ⊆ On
14		fnssres 4990	. . 3 ⊢ ((rec(𝐹, 𝐴) Fn On ∧ ω ⊆ On) → (rec(𝐹, 𝐴) ↾ ω) Fn ω)
15	12, 13, 14	sylancl 392	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐴) ↾ ω) Fn ω)
16		fveq2 5156	. . . . 5 ⊢ (𝑥 = ∅ → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘∅))
17		fveq2 5156	. . . . 5 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘∅))
18	16, 17	eqeq12d 2054	. . . 4 ⊢ (𝑥 = ∅ → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾ ω)‘∅)))
19		fveq2 5156	. . . . 5 ⊢ (𝑥 = 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘𝑦))
20		fveq2 5156	. . . . 5 ⊢ (𝑥 = 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦))
21	19, 20	eqeq12d 2054	. . . 4 ⊢ (𝑥 = 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)))
22		fveq2 5156	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (frec(𝐹, 𝐴)‘𝑥) = (frec(𝐹, 𝐴)‘suc 𝑦))
23		fveq2 5156	. . . . 5 ⊢ (𝑥 = suc 𝑦 → ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))
24	22, 23	eqeq12d 2054	. . . 4 ⊢ (𝑥 = suc 𝑦 → ((frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥) ↔ (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)))
25		frec0g 5961	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴)
26	8, 25	syl 14	. . . . 5 ⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = 𝐴)
27		peano1 4295	. . . . . . 7 ⊢ ∅ ∈ ω
28		fvres 5176	. . . . . . 7 ⊢ (∅ ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = (rec(𝐹, 𝐴)‘∅))
29	27, 28	ax-mp 7	. . . . . 6 ⊢ ((rec(𝐹, 𝐴) ↾ ω)‘∅) = (rec(𝐹, 𝐴)‘∅)
30		rdg0g 5953	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
31	8, 30	syl 14	. . . . . 6 ⊢ (𝜑 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
32	29, 31	syl5eq 2084	. . . . 5 ⊢ (𝜑 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴)
33	26, 32	eqtr4d 2075	. . . 4 ⊢ (𝜑 → (frec(𝐹, 𝐴)‘∅) = ((rec(𝐹, 𝐴) ↾ ω)‘∅))
34		simpr 103	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦))
35		fvres 5176	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦))
36	35	ad2antlr 458	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦))
37	34, 36	eqtrd 2072	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑦))
38	37	fveq2d 5160	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (𝐹‘(frec(𝐹, 𝐴)‘𝑦)) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦)))
39	7, 8	jca 290	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉))
40		frecsuc 5969	. . . . . . . . . . 11 ⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
41	40	3expa 1104	. . . . . . . . . 10 ⊢ (((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
42	39, 41	sylan 267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
43	42	adantr 261	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(frec(𝐹, 𝐴)‘𝑦)))
44	1	adantr 261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐹 Fn V)
45	8	adantr 261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝑉)
46		simpr 103	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ ω)
47		nnon 4310	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
48	46, 47	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → 𝑦 ∈ On)
49		frecrdg.inc	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥))
50	49	adantr 261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥))
51	44, 45, 48, 50	rdgisucinc 5950	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦)))
52	51	adantr 261	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (rec(𝐹, 𝐴)‘suc 𝑦) = (𝐹‘(rec(𝐹, 𝐴)‘𝑦)))
53	38, 43, 52	3eqtr4d 2082	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
54		peano2 4296	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
55		fvres 5176	. . . . . . . . 9 ⊢ (suc 𝑦 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
56	54, 55	syl 14	. . . . . . . 8 ⊢ (𝑦 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
57	56	ad2antlr 458	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦) = (rec(𝐹, 𝐴)‘suc 𝑦))
58	53, 57	eqtr4d 2075	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦)) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))
59	58	ex 108	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦)))
60	59	expcom 109	. . . 4 ⊢ (𝑦 ∈ ω → (𝜑 → ((frec(𝐹, 𝐴)‘𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑦) → (frec(𝐹, 𝐴)‘suc 𝑦) = ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝑦))))
61	18, 21, 24, 33, 60	finds2 4302	. . 3 ⊢ (𝑥 ∈ ω → (𝜑 → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥)))
62	61	impcom 116	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (frec(𝐹, 𝐴)‘𝑥) = ((rec(𝐹, 𝐴) ↾ ω)‘𝑥))
63	10, 15, 62	eqfnfvd 5246	1 ⊢ (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω))

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)