Theorem frecuzrdgfunlem 9791

Description: The recursive definition generator on upper integers produces a a function. (Contributed by Jim Kingdon, 24-Apr-2022.)

Hypotheses

Ref	Expression
frecuzrdgrclt.c	|- ( ph -> C e. ZZ )
frecuzrdgrclt.a	|- ( ph -> A e. S )
frecuzrdgrclt.t	|- ( ph -> S C_ T )
frecuzrdgrclt.f	|- ( ( ph /\ ( x e. ( ZZ>= ` C ) /\ y e. S ) ) -> ( x F y ) e. S )
frecuzrdgrclt.r	|- R = frec ( ( x e. ( ZZ>= ` C ) , y e. T |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. )
frecuzrdgfunlem.g	|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )

Assertion

Ref	Expression
frecuzrdgfunlem	|- ( ph -> Fun ran R )

Distinct variable groups:   x, C, y   x, F, y   x, S, y   x, T, y   ph, x, y   x, G, y   x, R, y

Allowed substitution hints:   A( x, y)

Proof of Theorem frecuzrdgfunlem

Dummy variables z w v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frecuzrdgrclt.c	. . . . . 6 |- ( ph -> C e. ZZ )
2		frecuzrdgrclt.a	. . . . . 6 |- ( ph -> A e. S )
3		frecuzrdgrclt.t	. . . . . 6 |- ( ph -> S C_ T )
4		frecuzrdgrclt.f	. . . . . 6 |- ( ( ph /\ ( x e. ( ZZ>= ` C ) /\ y e. S ) ) -> ( x F y ) e. S )
5		frecuzrdgrclt.r	. . . . . 6 |- R = frec ( ( x e. ( ZZ>= ` C ) , y e. T |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. )
6	1, 2, 3, 4, 5	frecuzrdgrclt 9787	. . . . 5 |- ( ph -> R : om --> ( ( ZZ>= ` C ) X. S ) )
7		frn 5155	. . . . 5 |- ( R : om --> ( ( ZZ>= ` C ) X. S ) -> ran R C_ ( ( ZZ>= ` C ) X. S ) )
8	6, 7	syl 14	. . . 4 |- ( ph -> ran R C_ ( ( ZZ>= ` C ) X. S ) )
9		xpss 4534	. . . 4 |- ( ( ZZ>= ` C ) X. S ) C_ ( _V X. _V )
10	8, 9	syl6ss 3035	. . 3 |- ( ph -> ran R C_ ( _V X. _V ) )
11		df-rel 4435	. . 3 |- ( Rel ran R <-> ran R C_ ( _V X. _V ) )
12	10, 11	sylibr 132	. 2 |- ( ph -> Rel ran R )
13		frecuzrdgfunlem.g	. . . . . . . . . 10 |- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )
14	1, 13	frec2uzf1od 9778	. . . . . . . . 9 |- ( ph -> G : om -1-1-onto-> ( ZZ>= ` C ) )
15		f1ocnvdm 5542	. . . . . . . . 9 |- ( ( G : om -1-1-onto-> ( ZZ>= ` C ) /\ v e. ( ZZ>= ` C ) ) -> ( `' G ` v ) e. om )
16	14, 15	sylan 277	. . . . . . . 8 |- ( ( ph /\ v e. ( ZZ>= ` C ) ) -> ( `' G ` v ) e. om )
17	6	ffvelrnda 5418	. . . . . . . 8 |- ( ( ph /\ ( `' G ` v ) e. om ) -> ( R ` ( `' G ` v ) ) e. ( ( ZZ>= ` C ) X. S ) )
18	16, 17	syldan 276	. . . . . . 7 |- ( ( ph /\ v e. ( ZZ>= ` C ) ) -> ( R ` ( `' G ` v ) ) e. ( ( ZZ>= ` C ) X. S ) )
19		xp2nd 5919	. . . . . . 7 |- ( ( R ` ( `' G ` v ) ) e. ( ( ZZ>= ` C ) X. S ) -> ( 2nd ` ( R ` ( `' G ` v ) ) ) e. S )
20	18, 19	syl 14	. . . . . 6 |- ( ( ph /\ v e. ( ZZ>= ` C ) ) -> ( 2nd ` ( R ` ( `' G ` v ) ) ) e. S )
21		ffn 5147	. . . . . . . . . 10 |- ( R : om --> ( ( ZZ>= ` C ) X. S ) -> R Fn om )
22		fvelrnb 5336	. . . . . . . . . 10 |- ( R Fn om -> ( <. v , z >. e. ran R <-> E. w e. om ( R ` w ) = <. v , z >. ) )
23	6, 21, 22	3syl 17	. . . . . . . . 9 |- ( ph -> ( <. v , z >. e. ran R <-> E. w e. om ( R ` w ) = <. v , z >. ) )
24	6	ffvelrnda 5418	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. om ) -> ( R ` w ) e. ( ( ZZ>= ` C ) X. S ) )
25		1st2nd2 5927	. . . . . . . . . . . . . . . . . . 19 |- ( ( R ` w ) e. ( ( ZZ>= ` C ) X. S ) -> ( R ` w ) = <. ( 1st ` ( R ` w ) ) , ( 2nd ` ( R ` w ) ) >. )
26	24, 25	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. om ) -> ( R ` w ) = <. ( 1st ` ( R ` w ) ) , ( 2nd ` ( R ` w ) ) >. )
27	1	adantr 270	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. om ) -> C e. ZZ )
28	2	adantr 270	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. om ) -> A e. S )
29	3	adantr 270	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. om ) -> S C_ T )
30	4	adantlr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w e. om ) /\ ( x e. ( ZZ>= ` C ) /\ y e. S ) ) -> ( x F y ) e. S )
31		simpr 108	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. om ) -> w e. om )
32	27, 28, 29, 30, 5, 31, 13	frecuzrdgg 9788	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. om ) -> ( 1st ` ( R ` w ) ) = ( G ` w ) )
33	32	opeq1d 3623	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. om ) -> <. ( 1st ` ( R ` w ) ) , ( 2nd ` ( R ` w ) ) >. = <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. )
34	26, 33	eqtrd 2120	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. om ) -> ( R ` w ) = <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. )
35	34	eqeq1d 2096	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w e. om ) -> ( ( R ` w ) = <. v , z >. <-> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. ) )
36		vex 2622	. . . . . . . . . . . . . . . . . 18 |- v e. _V
37		vex 2622	. . . . . . . . . . . . . . . . . 18 |- z e. _V
38	36, 37	opth2 4058	. . . . . . . . . . . . . . . . 17 |- ( <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. <-> ( ( G ` w ) = v /\ ( 2nd ` ( R ` w ) ) = z ) )
39	38	simplbi 268	. . . . . . . . . . . . . . . 16 |- ( <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. -> ( G ` w ) = v )
40	35, 39	syl6bi 161	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. om ) -> ( ( R ` w ) = <. v , z >. -> ( G ` w ) = v ) )
41		f1ocnvfv 5540	. . . . . . . . . . . . . . . 16 |- ( ( G : om -1-1-onto-> ( ZZ>= ` C ) /\ w e. om ) -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
42	14, 41	sylan 277	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. om ) -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
43	40, 42	syld 44	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. om ) -> ( ( R ` w ) = <. v , z >. -> ( `' G ` v ) = w ) )
44		fveq2 5289	. . . . . . . . . . . . . . 15 |- ( ( `' G ` v ) = w -> ( R ` ( `' G ` v ) ) = ( R ` w ) )
45	44	fveq2d 5293	. . . . . . . . . . . . . 14 |- ( ( `' G ` v ) = w -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) )
46	43, 45	syl6 33	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. om ) -> ( ( R ` w ) = <. v , z >. -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) ) )
47	46	imp 122	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. om ) /\ ( R ` w ) = <. v , z >. ) -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) )
48	36, 37	op2ndd 5902	. . . . . . . . . . . . 13 |- ( ( R ` w ) = <. v , z >. -> ( 2nd ` ( R ` w ) ) = z )
49	48	adantl 271	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. om ) /\ ( R ` w ) = <. v , z >. ) -> ( 2nd ` ( R ` w ) ) = z )
50	47, 49	eqtr2d 2121	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. om ) /\ ( R ` w ) = <. v , z >. ) -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) )
51	50	ex 113	. . . . . . . . . 10 |- ( ( ph /\ w e. om ) -> ( ( R ` w ) = <. v , z >. -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
52	51	rexlimdva 2489	. . . . . . . . 9 |- ( ph -> ( E. w e. om ( R ` w ) = <. v , z >. -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
53	23, 52	sylbid 148	. . . . . . . 8 |- ( ph -> ( <. v , z >. e. ran R -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
54	53	alrimiv 1802	. . . . . . 7 |- ( ph -> A. z ( <. v , z >. e. ran R -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
55	54	adantr 270	. . . . . 6 |- ( ( ph /\ v e. ( ZZ>= ` C ) ) -> A. z ( <. v , z >. e. ran R -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
56		eqeq2 2097	. . . . . . . . 9 |- ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( z = w <-> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
57	56	imbi2d 228	. . . . . . . 8 |- ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( ( <. v , z >. e. ran R -> z = w ) <-> ( <. v , z >. e. ran R -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) ) )
58	57	albidv 1752	. . . . . . 7 |- ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( A. z ( <. v , z >. e. ran R -> z = w ) <-> A. z ( <. v , z >. e. ran R -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) ) )
59	58	spcegv 2707	. . . . . 6 |- ( ( 2nd ` ( R ` ( `' G ` v ) ) ) e. S -> ( A. z ( <. v , z >. e. ran R -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) -> E. w A. z ( <. v , z >. e. ran R -> z = w ) ) )
60	20, 55, 59	sylc 61	. . . . 5 |- ( ( ph /\ v e. ( ZZ>= ` C ) ) -> E. w A. z ( <. v , z >. e. ran R -> z = w ) )
61		nfv 1466	. . . . . 6 |- F/ w <. v , z >. e. ran R
62	61	mo2r 2000	. . . . 5 |- ( E. w A. z ( <. v , z >. e. ran R -> z = w ) -> E* z <. v , z >. e. ran R )
63	60, 62	syl 14	. . . 4 |- ( ( ph /\ v e. ( ZZ>= ` C ) ) -> E* z <. v , z >. e. ran R )
64	1, 2, 3, 4, 5	frecuzrdgdom 9790	. . . . . 6 |- ( ph -> dom ran R = ( ZZ>= ` C ) )
65	64	eleq2d 2157	. . . . 5 |- ( ph -> ( v e. dom ran R <-> v e. ( ZZ>= ` C ) ) )
66	65	pm5.32i 442	. . . 4 |- ( ( ph /\ v e. dom ran R ) <-> ( ph /\ v e. ( ZZ>= ` C ) ) )
67		df-br 3838	. . . . 5 |- ( v ran R z <-> <. v , z >. e. ran R )
68	67	mobii 1985	. . . 4 |- ( E* z v ran R z <-> E* z <. v , z >. e. ran R )
69	63, 66, 68	3imtr4i 199	. . 3 |- ( ( ph /\ v e. dom ran R ) -> E* z v ran R z )
70	69	ralrimiva 2446	. 2 |- ( ph -> A. v e. dom ran R E* z v ran R z )
71		dffun7 5028	. 2 |- ( Fun ran R <-> ( Rel ran R /\ A. v e. dom ran R E* z v ran R z ) )
72	12, 70, 71	sylanbrc 408	1 |- ( ph -> Fun ran R )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   A.wal 1287   = wceq 1289   E.wex 1426   e. wcel 1438   E*wmo 1949   A.wral 2359   E.wrex 2360   _Vcvv 2619   C_ wss 2997   <.cop 3444   class class class wbr 3837   |-> cmpt 3891   omcom 4395   X. cxp 4426   `'ccnv 4427   dom cdm 4428   ran crn 4429   Rel wrel 4433   Fun wfun 4996   Fn wfn 4997   -->wf 4998   -1-1-onto->wf1o 5001   ` cfv 5002  (class class class)co 5634   |-> cmpt2 5636   1stc1st 5891   2ndc2nd 5892  freccfrec 6137   1c1 7330   + caddc 7332   ZZcz 8720   ZZ>=cuz 8988

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393  ax-cnex 7415  ax-resscn 7416  ax-1cn 7417  ax-1re 7418  ax-icn 7419  ax-addcl 7420  ax-addrcl 7421  ax-mulcl 7422  ax-addcom 7424  ax-addass 7426  ax-distr 7428  ax-i2m1 7429  ax-0lt1 7430  ax-0id 7432  ax-rnegex 7433  ax-cnre 7435  ax-pre-ltirr 7436  ax-pre-ltwlin 7437  ax-pre-lttrn 7438  ax-pre-ltadd 7440

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-iord 4184  df-on 4186  df-ilim 4187  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-riota 5590  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-recs 6052  df-frec 6138  df-pnf 7503  df-mnf 7504  df-xr 7505  df-ltxr 7506  df-le 7507  df-sub 7634  df-neg 7635  df-inn 8395  df-n0 8644  df-z 8721  df-uz 8989

This theorem is referenced by:  frecuzrdgfun  9792