Theorem fnfrec 6321

Description: The recursive function generator is a function over the finite cardinals. (Contributed by Scott Fenton, 31-Jul-2019.)

Hypotheses

Ref	Expression
fnfrec.1	|- F = FRec (G, I)
fnfrec.2	|- (ph -> G e. Funs )
fnfrec.3	|- (ph -> I e. dom G)
fnfrec.4	|- (ph -> ran G C_ dom G)

Assertion

Ref	Expression
fnfrec	|- (ph -> F Fn Nn )

Proof of Theorem fnfrec

Dummy variables x y z w t a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breldm 4912	. . . . . . . . . 10 |- (xFy -> x e. dom F)
2	1	adantl 452	. . . . . . . . 9 |- ((ph /\ xFy) -> x e. dom F)
3		fnfrec.1	. . . . . . . . . . 11 |- F = FRec (G, I)
4		fnfrec.2	. . . . . . . . . . 11 |- (ph -> G e. Funs )
5		fnfrec.3	. . . . . . . . . . 11 |- (ph -> I e. dom G)
6		fnfrec.4	. . . . . . . . . . 11 |- (ph -> ran G C_ dom G)
7	3, 4, 5, 6	dmfrec 6317	. . . . . . . . . 10 |- (ph -> dom F = Nn )
8	7	adantr 451	. . . . . . . . 9 |- ((ph /\ xFy) -> dom F = Nn )
9	2, 8	eleqtrd 2429	. . . . . . . 8 |- ((ph /\ xFy) -> x e. Nn )
10	9	adantrr 697	. . . . . . 7 |- ((ph /\ (xFy /\ xFz)) -> x e. Nn )
11	3	frecexg 6313	. . . . . . . . . . . 12 |- (G e. Funs -> F e. _V)
12		fnfreclem1 6318	. . . . . . . . . . . 12 |- (F e. _V -> {w | A.yA.z((wFy /\ wFz) -> y = z)} e. _V)
13	4, 11, 12	3syl 18	. . . . . . . . . . 11 |- (ph -> {w | A.yA.z((wFy /\ wFz) -> y = z)} e. _V)
14		breq1 4643	. . . . . . . . . . . . . 14 |- (w = 0c -> (wFy <-> 0cFy))
15		breq1 4643	. . . . . . . . . . . . . 14 |- (w = 0c -> (wFz <-> 0cFz))
16	14, 15	anbi12d 691	. . . . . . . . . . . . 13 |- (w = 0c -> ((wFy /\ wFz) <-> (0cFy /\ 0cFz)))
17	16	imbi1d 308	. . . . . . . . . . . 12 |- (w = 0c -> (((wFy /\ wFz) -> y = z) <-> ((0cFy /\ 0cFz) -> y = z)))
18	17	2albidv 1627	. . . . . . . . . . 11 |- (w = 0c -> (A.yA.z((wFy /\ wFz) -> y = z) <-> A.yA.z((0cFy /\ 0cFz) -> y = z)))
19		breq1 4643	. . . . . . . . . . . . . 14 |- (w = t -> (wFy <-> tFy))
20		breq1 4643	. . . . . . . . . . . . . 14 |- (w = t -> (wFz <-> tFz))
21	19, 20	anbi12d 691	. . . . . . . . . . . . 13 |- (w = t -> ((wFy /\ wFz) <-> (tFy /\ tFz)))
22	21	imbi1d 308	. . . . . . . . . . . 12 |- (w = t -> (((wFy /\ wFz) -> y = z) <-> ((tFy /\ tFz) -> y = z)))
23	22	2albidv 1627	. . . . . . . . . . 11 |- (w = t -> (A.yA.z((wFy /\ wFz) -> y = z) <-> A.yA.z((tFy /\ tFz) -> y = z)))
24		breq1 4643	. . . . . . . . . . . . . . 15 |- (w = (t +o 1c) -> (wFy <-> (t +o 1c)Fy))
25		breq1 4643	. . . . . . . . . . . . . . 15 |- (w = (t +o 1c) -> (wFz <-> (t +o 1c)Fz))
26	24, 25	anbi12d 691	. . . . . . . . . . . . . 14 |- (w = (t +o 1c) -> ((wFy /\ wFz) <-> ((t +o 1c)Fy /\ (t +o 1c)Fz)))
27	26	imbi1d 308	. . . . . . . . . . . . 13 |- (w = (t +o 1c) -> (((wFy /\ wFz) -> y = z) <-> (((t +o 1c)Fy /\ (t +o 1c)Fz) -> y = z)))
28	27	2albidv 1627	. . . . . . . . . . . 12 |- (w = (t +o 1c) -> (A.yA.z((wFy /\ wFz) -> y = z) <-> A.yA.z(((t +o 1c)Fy /\ (t +o 1c)Fz) -> y = z)))
29		breq2 4644	. . . . . . . . . . . . . . 15 |- (y = a -> ((t +o 1c)Fy <-> (t +o 1c)Fa))
30		breq2 4644	. . . . . . . . . . . . . . 15 |- (z = b -> ((t +o 1c)Fz <-> (t +o 1c)Fb))
31	29, 30	bi2anan9 843	. . . . . . . . . . . . . 14 |- ((y = a /\ z = b) -> (((t +o 1c)Fy /\ (t +o 1c)Fz) <-> ((t +o 1c)Fa /\ (t +o 1c)Fb)))
32		eqeq12 2365	. . . . . . . . . . . . . 14 |- ((y = a /\ z = b) -> (y = z <-> a = b))
33	31, 32	imbi12d 311	. . . . . . . . . . . . 13 |- ((y = a /\ z = b) -> ((((t +o 1c)Fy /\ (t +o 1c)Fz) -> y = z) <-> (((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b)))
34	33	cbval2v 2006	. . . . . . . . . . . 12 |- (A.yA.z(((t +o 1c)Fy /\ (t +o 1c)Fz) -> y = z) <-> A.aA.b(((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b))
35	28, 34	syl6bb 252	. . . . . . . . . . 11 |- (w = (t +o 1c) -> (A.yA.z((wFy /\ wFz) -> y = z) <-> A.aA.b(((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b)))
36		breq1 4643	. . . . . . . . . . . . . 14 |- (w = x -> (wFy <-> xFy))
37		breq1 4643	. . . . . . . . . . . . . 14 |- (w = x -> (wFz <-> xFz))
38	36, 37	anbi12d 691	. . . . . . . . . . . . 13 |- (w = x -> ((wFy /\ wFz) <-> (xFy /\ xFz)))
39	38	imbi1d 308	. . . . . . . . . . . 12 |- (w = x -> (((wFy /\ wFz) -> y = z) <-> ((xFy /\ xFz) -> y = z)))
40	39	2albidv 1627	. . . . . . . . . . 11 |- (w = x -> (A.yA.z((wFy /\ wFz) -> y = z) <-> A.yA.z((xFy /\ xFz) -> y = z)))
41	3, 4, 5, 6	fnfreclem2 6319	. . . . . . . . . . . . . . . 16 |- (ph -> (0cFy -> y = I))
42	41	imp 418	. . . . . . . . . . . . . . 15 |- ((ph /\ 0cFy) -> y = I)
43	42	adantrr 697	. . . . . . . . . . . . . 14 |- ((ph /\ (0cFy /\ 0cFz)) -> y = I)
44	3, 4, 5, 6	fnfreclem2 6319	. . . . . . . . . . . . . . . 16 |- (ph -> (0cFz -> z = I))
45	44	imp 418	. . . . . . . . . . . . . . 15 |- ((ph /\ 0cFz) -> z = I)
46	45	adantrl 696	. . . . . . . . . . . . . 14 |- ((ph /\ (0cFy /\ 0cFz)) -> z = I)
47	43, 46	eqtr4d 2388	. . . . . . . . . . . . 13 |- ((ph /\ (0cFy /\ 0cFz)) -> y = z)
48	47	ex 423	. . . . . . . . . . . 12 |- (ph -> ((0cFy /\ 0cFz) -> y = z))
49	48	alrimivv 1632	. . . . . . . . . . 11 |- (ph -> A.yA.z((0cFy /\ 0cFz) -> y = z))
50	4	ad2antrr 706	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fa) -> G e. Funs )
51	5	ad2antrr 706	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fa) -> I e. dom G)
52	6	ad2antrr 706	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fa) -> ran G C_ dom G)
53		simplr 731	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fa) -> t e. Nn )
54		simpr 447	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fa) -> (t +o 1c)Fa)
55	3, 50, 51, 52, 53, 54	fnfreclem3 6320	. . . . . . . . . . . . . . . . . . 19 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fa) -> E.y(tFy /\ yGa))
56	55	adantlrr 701	. . . . . . . . . . . . . . . . . 18 |- (((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) /\ (t +o 1c)Fa) -> E.y(tFy /\ yGa))
57	56	ex 423	. . . . . . . . . . . . . . . . 17 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> ((t +o 1c)Fa -> E.y(tFy /\ yGa)))
58	4	ad2antrr 706	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fb) -> G e. Funs )
59	5	ad2antrr 706	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fb) -> I e. dom G)
60	6	ad2antrr 706	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fb) -> ran G C_ dom G)
61		simplr 731	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fb) -> t e. Nn )
62		simpr 447	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fb) -> (t +o 1c)Fb)
63	3, 58, 59, 60, 61, 62	fnfreclem3 6320	. . . . . . . . . . . . . . . . . . 19 |- (((ph /\ t e. Nn ) /\ (t +o 1c)Fb) -> E.z(tFz /\ zGb))
64	63	adantlrr 701	. . . . . . . . . . . . . . . . . 18 |- (((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) /\ (t +o 1c)Fb) -> E.z(tFz /\ zGb))
65	64	ex 423	. . . . . . . . . . . . . . . . 17 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> ((t +o 1c)Fb -> E.z(tFz /\ zGb)))
66	57, 65	anim12d 546	. . . . . . . . . . . . . . . 16 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> (((t +o 1c)Fa /\ (t +o 1c)Fb) -> (E.y(tFy /\ yGa) /\ E.z(tFz /\ zGb))))
67		eeanv 1913	. . . . . . . . . . . . . . . 16 |- (E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb)) <-> (E.y(tFy /\ yGa) /\ E.z(tFz /\ zGb)))
68	66, 67	syl6ibr 218	. . . . . . . . . . . . . . 15 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> (((t +o 1c)Fa /\ (t +o 1c)Fb) -> E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb))))
69		19.29 1596	. . . . . . . . . . . . . . . . . . 19 |- ((A.yA.z((tFy /\ tFz) -> y = z) /\ E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb))) -> E.y(A.z((tFy /\ tFz) -> y = z) /\ E.z((tFy /\ yGa) /\ (tFz /\ zGb))))
70		19.29 1596	. . . . . . . . . . . . . . . . . . . 20 |- ((A.z((tFy /\ tFz) -> y = z) /\ E.z((tFy /\ yGa) /\ (tFz /\ zGb))) -> E.z(((tFy /\ tFz) -> y = z) /\ ((tFy /\ yGa) /\ (tFz /\ zGb))))
71	70	eximi 1576	. . . . . . . . . . . . . . . . . . 19 |- (E.y(A.z((tFy /\ tFz) -> y = z) /\ E.z((tFy /\ yGa) /\ (tFz /\ zGb))) -> E.yE.z(((tFy /\ tFz) -> y = z) /\ ((tFy /\ yGa) /\ (tFz /\ zGb))))
72	69, 71	syl 15	. . . . . . . . . . . . . . . . . 18 |- ((A.yA.z((tFy /\ tFz) -> y = z) /\ E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb))) -> E.yE.z(((tFy /\ tFz) -> y = z) /\ ((tFy /\ yGa) /\ (tFz /\ zGb))))
73		pm3.35 570	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((tFy /\ tFz) /\ ((tFy /\ tFz) -> y = z)) -> y = z)
74		breq1 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y = z -> (yGa <-> zGa))
75	74	anbi1d 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = z -> ((yGa /\ zGb) <-> (zGa /\ zGb)))
76	75	biimpa 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((y = z /\ (yGa /\ zGb)) -> (zGa /\ zGb))
77		elfunsi 5832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (G e. Funs -> Fun G)
78		funbrfv 5357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (Fun G -> (zGa -> (G` z) = a))
79	4, 77, 78	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> (zGa -> (G` z) = a))
80		funbrfv 5357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (Fun G -> (zGb -> (G` z) = b))
81	4, 77, 80	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> (zGb -> (G` z) = b))
82	79, 81	anim12d 546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (ph -> ((zGa /\ zGb) -> ((G` z) = a /\ (G` z) = b)))
83		eqtr2 2371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((G` z) = a /\ (G` z) = b) -> a = b)
84	76, 82, 83	syl56 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (ph -> ((y = z /\ (yGa /\ zGb)) -> a = b))
85	84	exp3a 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (ph -> (y = z -> ((yGa /\ zGb) -> a = b)))
86	73, 85	syl5 28	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (ph -> (((tFy /\ tFz) /\ ((tFy /\ tFz) -> y = z)) -> ((yGa /\ zGb) -> a = b)))
87	86	exp3a 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (ph -> ((tFy /\ tFz) -> (((tFy /\ tFz) -> y = z) -> ((yGa /\ zGb) -> a = b))))
88	87	com34 77	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (ph -> ((tFy /\ tFz) -> ((yGa /\ zGb) -> (((tFy /\ tFz) -> y = z) -> a = b))))
89	88	imp3a 420	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (ph -> (((tFy /\ tFz) /\ (yGa /\ zGb)) -> (((tFy /\ tFz) -> y = z) -> a = b)))
90	89	com12 27	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((tFy /\ tFz) /\ (yGa /\ zGb)) -> (ph -> (((tFy /\ tFz) -> y = z) -> a = b)))
91	90	an4s 799	. . . . . . . . . . . . . . . . . . . . . 22 |- (((tFy /\ yGa) /\ (tFz /\ zGb)) -> (ph -> (((tFy /\ tFz) -> y = z) -> a = b)))
92	91	com3l 75	. . . . . . . . . . . . . . . . . . . . 21 |- (ph -> (((tFy /\ tFz) -> y = z) -> (((tFy /\ yGa) /\ (tFz /\ zGb)) -> a = b)))
93	92	imp3a 420	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> ((((tFy /\ tFz) -> y = z) /\ ((tFy /\ yGa) /\ (tFz /\ zGb))) -> a = b))
94	93	exlimdvv 1637	. . . . . . . . . . . . . . . . . . 19 |- (ph -> (E.yE.z(((tFy /\ tFz) -> y = z) /\ ((tFy /\ yGa) /\ (tFz /\ zGb))) -> a = b))
95	94	adantr 451	. . . . . . . . . . . . . . . . . 18 |- ((ph /\ t e. Nn ) -> (E.yE.z(((tFy /\ tFz) -> y = z) /\ ((tFy /\ yGa) /\ (tFz /\ zGb))) -> a = b))
96	72, 95	syl5 28	. . . . . . . . . . . . . . . . 17 |- ((ph /\ t e. Nn ) -> ((A.yA.z((tFy /\ tFz) -> y = z) /\ E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb))) -> a = b))
97	96	exp3a 425	. . . . . . . . . . . . . . . 16 |- ((ph /\ t e. Nn ) -> (A.yA.z((tFy /\ tFz) -> y = z) -> (E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb)) -> a = b)))
98	97	impr 602	. . . . . . . . . . . . . . 15 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> (E.yE.z((tFy /\ yGa) /\ (tFz /\ zGb)) -> a = b))
99	68, 98	syld 40	. . . . . . . . . . . . . 14 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> (((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b))
100	99	alrimivv 1632	. . . . . . . . . . . . 13 |- ((ph /\ (t e. Nn /\ A.yA.z((tFy /\ tFz) -> y = z))) -> A.aA.b(((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b))
101	100	expr 598	. . . . . . . . . . . 12 |- ((ph /\ t e. Nn ) -> (A.yA.z((tFy /\ tFz) -> y = z) -> A.aA.b(((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b)))
102	101	ancoms 439	. . . . . . . . . . 11 |- ((t e. Nn /\ ph) -> (A.yA.z((tFy /\ tFz) -> y = z) -> A.aA.b(((t +o 1c)Fa /\ (t +o 1c)Fb) -> a = b)))
103	13, 18, 23, 35, 40, 49, 102	findsd 4411	. . . . . . . . . 10 |- ((x e. Nn /\ ph) -> A.yA.z((xFy /\ xFz) -> y = z))
104	103	19.21bbi 1865	. . . . . . . . 9 |- ((x e. Nn /\ ph) -> ((xFy /\ xFz) -> y = z))
105	104	ex 423	. . . . . . . 8 |- (x e. Nn -> (ph -> ((xFy /\ xFz) -> y = z)))
106	105	imp3a 420	. . . . . . 7 |- (x e. Nn -> ((ph /\ (xFy /\ xFz)) -> y = z))
107	10, 106	mpcom 32	. . . . . 6 |- ((ph /\ (xFy /\ xFz)) -> y = z)
108	107	ex 423	. . . . 5 |- (ph -> ((xFy /\ xFz) -> y = z))
109	108	alrimivv 1632	. . . 4 |- (ph -> A.yA.z((xFy /\ xFz) -> y = z))
110	109	alrimiv 1631	. . 3 |- (ph -> A.xA.yA.z((xFy /\ xFz) -> y = z))
111		dffun2 5120	. . 3 |- (Fun F <-> A.xA.yA.z((xFy /\ xFz) -> y = z))
112	110, 111	sylibr 203	. 2 |- (ph -> Fun F)
113		df-fn 4791	. 2 |- (F Fn Nn <-> (Fun F /\ dom F = Nn ))
114	112, 7, 113	sylanbrc 645	1 |- (ph -> F Fn Nn )

Syntax hints:   -> wi 4   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  _Vcvv 2860   C_ wss 3258  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +o cplc 4376   class class class wbr 4640  dom cdm 4773  ran crn 4774  Fun wfun 4776   Fn wfn 4777  ` cfv 4782   Funs cfuns 5760   FRec cfrec 6310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-csb 3138  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-iun 3972  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-fo 4794  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-pprod 5739  df-fix 5741  df-cup 5743  df-disj 5745  df-addcfn 5747  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-clos1 5874  df-frec 6311

This theorem is referenced by:  frec0  6322  frecsuc  6323