Theorem frecrdg 5908

Description: Transfinite recursion restricted to omega.

Given a suitable characteristic function, df-frec 5898 produces the same results as df-irdg 5878 restricted to 𝜔. (Contributed by Jim Kingdon, 29-Aug-2019.)

Hypotheses

Ref	Expression
frecrdg.1	⊢ (φ → 𝐹 Fn V)
frecrdg.2	⊢ (φ → A ∈ 𝑉)
frecrdg.inc	⊢ (φ → ∀x x ⊆ (𝐹‘x))

Assertion

Ref	Expression
frecrdg	⊢ (φ → frec(𝐹, A) = (rec(𝐹, A) ↾ 𝜔))

Distinct variable groups:   x,A   x,𝐹   x,𝑉   φ,x

Proof of Theorem frecrdg

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		frecrdg.1	. . 3 ⊢ (φ → 𝐹 Fn V)
2		frecrdg.2	. . 3 ⊢ (φ → A ∈ 𝑉)
3		frecfnom 5901	. . 3 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → frec(𝐹, A) Fn 𝜔)
4	1, 2, 3	syl2anc 393	. 2 ⊢ (φ → frec(𝐹, A) Fn 𝜔)
5		rdgifnon 5887	. . . 4 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → rec(𝐹, A) Fn On)
6	1, 2, 5	syl2anc 393	. . 3 ⊢ (φ → rec(𝐹, A) Fn On)
7		omsson 4262	. . 3 ⊢ 𝜔 ⊆ On
8		fnssres 4938	. . 3 ⊢ ((rec(𝐹, A) Fn On ∧ 𝜔 ⊆ On) → (rec(𝐹, A) ↾ 𝜔) Fn 𝜔)
9	6, 7, 8	sylancl 394	. 2 ⊢ (φ → (rec(𝐹, A) ↾ 𝜔) Fn 𝜔)
10		fveq2 5103	. . . . 5 ⊢ (x = ∅ → (frec(𝐹, A)‘x) = (frec(𝐹, A)‘∅))
11		fveq2 5103	. . . . 5 ⊢ (x = ∅ → ((rec(𝐹, A) ↾ 𝜔)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘∅))
12	10, 11	eqeq12d 2036	. . . 4 ⊢ (x = ∅ → ((frec(𝐹, A)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘x) ↔ (frec(𝐹, A)‘∅) = ((rec(𝐹, A) ↾ 𝜔)‘∅)))
13		fveq2 5103	. . . . 5 ⊢ (x = y → (frec(𝐹, A)‘x) = (frec(𝐹, A)‘y))
14		fveq2 5103	. . . . 5 ⊢ (x = y → ((rec(𝐹, A) ↾ 𝜔)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘y))
15	13, 14	eqeq12d 2036	. . . 4 ⊢ (x = y → ((frec(𝐹, A)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘x) ↔ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)))
16		fveq2 5103	. . . . 5 ⊢ (x = suc y → (frec(𝐹, A)‘x) = (frec(𝐹, A)‘suc y))
17		fveq2 5103	. . . . 5 ⊢ (x = suc y → ((rec(𝐹, A) ↾ 𝜔)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘suc y))
18	16, 17	eqeq12d 2036	. . . 4 ⊢ (x = suc y → ((frec(𝐹, A)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘x) ↔ (frec(𝐹, A)‘suc y) = ((rec(𝐹, A) ↾ 𝜔)‘suc y)))
19		frec0g 5902	. . . . . 6 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (frec(𝐹, A)‘∅) = A)
20	1, 2, 19	syl2anc 393	. . . . 5 ⊢ (φ → (frec(𝐹, A)‘∅) = A)
21		peano1 4244	. . . . . . 7 ⊢ ∅ ∈ 𝜔
22		fvres 5123	. . . . . . 7 ⊢ (∅ ∈ 𝜔 → ((rec(𝐹, A) ↾ 𝜔)‘∅) = (rec(𝐹, A)‘∅))
23	21, 22	ax-mp 7	. . . . . 6 ⊢ ((rec(𝐹, A) ↾ 𝜔)‘∅) = (rec(𝐹, A)‘∅)
24		rdgi0g 5886	. . . . . . 7 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (rec(𝐹, A)‘∅) = A)
25	1, 2, 24	syl2anc 393	. . . . . 6 ⊢ (φ → (rec(𝐹, A)‘∅) = A)
26	23, 25	syl5eq 2066	. . . . 5 ⊢ (φ → ((rec(𝐹, A) ↾ 𝜔)‘∅) = A)
27	20, 26	eqtr4d 2057	. . . 4 ⊢ (φ → (frec(𝐹, A)‘∅) = ((rec(𝐹, A) ↾ 𝜔)‘∅))
28		ax-ia2 100	. . . . . . . . . 10 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y))
29		fvres 5123	. . . . . . . . . . 11 ⊢ (y ∈ 𝜔 → ((rec(𝐹, A) ↾ 𝜔)‘y) = (rec(𝐹, A)‘y))
30	29	ad2antlr 462	. . . . . . . . . 10 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → ((rec(𝐹, A) ↾ 𝜔)‘y) = (rec(𝐹, A)‘y))
31	28, 30	eqtrd 2054	. . . . . . . . 9 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘y) = (rec(𝐹, A)‘y))
32	31	fveq2d 5107	. . . . . . . 8 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (𝐹‘(frec(𝐹, A)‘y)) = (𝐹‘(rec(𝐹, A)‘y)))
33	1, 2	jca 290	. . . . . . . . . 10 ⊢ (φ → (𝐹 Fn V ∧ A ∈ 𝑉))
34		frecsuc 5907	. . . . . . . . . . 11 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ y ∈ 𝜔) → (frec(𝐹, A)‘suc y) = (𝐹‘(frec(𝐹, A)‘y)))
35	34	3expa 1090	. . . . . . . . . 10 ⊢ (((𝐹 Fn V ∧ A ∈ 𝑉) ∧ y ∈ 𝜔) → (frec(𝐹, A)‘suc y) = (𝐹‘(frec(𝐹, A)‘y)))
36	33, 35	sylan 267	. . . . . . . . 9 ⊢ ((φ ∧ y ∈ 𝜔) → (frec(𝐹, A)‘suc y) = (𝐹‘(frec(𝐹, A)‘y)))
37	36	adantr 261	. . . . . . . 8 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘suc y) = (𝐹‘(frec(𝐹, A)‘y)))
38	1	adantr 261	. . . . . . . . . 10 ⊢ ((φ ∧ y ∈ 𝜔) → 𝐹 Fn V)
39	2	adantr 261	. . . . . . . . . 10 ⊢ ((φ ∧ y ∈ 𝜔) → A ∈ 𝑉)
40		ax-ia2 100	. . . . . . . . . . 11 ⊢ ((φ ∧ y ∈ 𝜔) → y ∈ 𝜔)
41		nnon 4259	. . . . . . . . . . 11 ⊢ (y ∈ 𝜔 → y ∈ On)
42	40, 41	syl 14	. . . . . . . . . 10 ⊢ ((φ ∧ y ∈ 𝜔) → y ∈ On)
43		frecrdg.inc	. . . . . . . . . . 11 ⊢ (φ → ∀x x ⊆ (𝐹‘x))
44	43	adantr 261	. . . . . . . . . 10 ⊢ ((φ ∧ y ∈ 𝜔) → ∀x x ⊆ (𝐹‘x))
45	38, 39, 42, 44	rdgisucinc 5892	. . . . . . . . 9 ⊢ ((φ ∧ y ∈ 𝜔) → (rec(𝐹, A)‘suc y) = (𝐹‘(rec(𝐹, A)‘y)))
46	45	adantr 261	. . . . . . . 8 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (rec(𝐹, A)‘suc y) = (𝐹‘(rec(𝐹, A)‘y)))
47	32, 37, 46	3eqtr4d 2064	. . . . . . 7 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘suc y) = (rec(𝐹, A)‘suc y))
48		peano2 4245	. . . . . . . . 9 ⊢ (y ∈ 𝜔 → suc y ∈ 𝜔)
49		fvres 5123	. . . . . . . . 9 ⊢ (suc y ∈ 𝜔 → ((rec(𝐹, A) ↾ 𝜔)‘suc y) = (rec(𝐹, A)‘suc y))
50	48, 49	syl 14	. . . . . . . 8 ⊢ (y ∈ 𝜔 → ((rec(𝐹, A) ↾ 𝜔)‘suc y) = (rec(𝐹, A)‘suc y))
51	50	ad2antlr 462	. . . . . . 7 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → ((rec(𝐹, A) ↾ 𝜔)‘suc y) = (rec(𝐹, A)‘suc y))
52	47, 51	eqtr4d 2057	. . . . . 6 ⊢ (((φ ∧ y ∈ 𝜔) ∧ (frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y)) → (frec(𝐹, A)‘suc y) = ((rec(𝐹, A) ↾ 𝜔)‘suc y))
53	52	ex 108	. . . . 5 ⊢ ((φ ∧ y ∈ 𝜔) → ((frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y) → (frec(𝐹, A)‘suc y) = ((rec(𝐹, A) ↾ 𝜔)‘suc y)))
54	53	expcom 109	. . . 4 ⊢ (y ∈ 𝜔 → (φ → ((frec(𝐹, A)‘y) = ((rec(𝐹, A) ↾ 𝜔)‘y) → (frec(𝐹, A)‘suc y) = ((rec(𝐹, A) ↾ 𝜔)‘suc y))))
55	12, 15, 18, 27, 54	finds2 4251	. . 3 ⊢ (x ∈ 𝜔 → (φ → (frec(𝐹, A)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘x)))
56	55	impcom 116	. 2 ⊢ ((φ ∧ x ∈ 𝜔) → (frec(𝐹, A)‘x) = ((rec(𝐹, A) ↾ 𝜔)‘x))
57	4, 9, 56	eqfnfvd 5193	1 ⊢ (φ → frec(𝐹, A) = (rec(𝐹, A) ↾ 𝜔))

Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1226   = wceq 1228   ∈ wcel 1374  Vcvv 2535   ⊆ wss 2894  ∅c0 3201  Oncon0 4049  suc csuc 4051  𝜔com 4240   ↾ cres 4274   Fn wfn 4824  ‘cfv 4829  reccrdg 5877  freccfrec 5897

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 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-coll 3846  ax-sep 3849  ax-nul 3857  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204  ax-iinf 4238

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-csb 2830  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-int 3590  df-iun 3633  df-br 3739  df-opab 3793  df-mpt 3794  df-tr 3829  df-id 4004  df-iord 4052  df-on 4054  df-suc 4057  df-iom 4241  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-fo 4835  df-f1o 4836  df-fv 4837  df-recs 5842  df-irdg 5878  df-frec 5898

This theorem is referenced by: (None)