Theorem tfrcllembacc 6182

Description: Lemma for tfrcl 6191. Each element of B is an acceptable function. (Contributed by Jim Kingdon, 25-Mar-2022.)

Hypotheses

Ref	Expression
tfrcl.f	|- F = recs ( G )
tfrcl.g	|- ( ph -> Fun G )
tfrcl.x	|- ( ph -> Ord X )
tfrcl.ex	|- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )
tfrcllemsucfn.1	|- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }
tfrcllembacc.3	|- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }
tfrcllembacc.u	|- ( ( ph /\ x e. U. X ) -> suc x e. X )
tfrcllembacc.4	|- ( ph -> D e. X )
tfrcllembacc.5	|- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )

Assertion

Ref	Expression
tfrcllembacc	|- ( ph -> B C_ A )

Distinct variable groups:   A, f, g, h, x, y, z   D, f, g, x, y   f, G, x, y   S, f, x, y   f, X, x   ph, f, g, h, x, y, z

Allowed substitution hints:   ph( w)   A( w)   B( x, y, z, w, f, g, h)   D( z, w, h)   S( z, w, g, h)   F( x, y, z, w, f, g, h)   G( z, w, g, h)   X( y, z, w, g, h)

Proof of Theorem tfrcllembacc

Step	Hyp	Ref	Expression
1		tfrcllembacc.3	. 2 |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }
2		simpr3 957	. . . . . . 7 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> h = ( g u. { <. z , ( G ` g ) >. } ) )
3		tfrcl.f	. . . . . . . 8 |- F = recs ( G )
4		tfrcl.g	. . . . . . . . 9 |- ( ph -> Fun G )
5	4	ad2antrr 475	. . . . . . . 8 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> Fun G )
6		tfrcl.x	. . . . . . . . 9 |- ( ph -> Ord X )
7	6	ad2antrr 475	. . . . . . . 8 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> Ord X )
8		simp1ll 1012	. . . . . . . . 9 |- ( ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) /\ x e. X /\ f : x --> S ) -> ph )
9		tfrcl.ex	. . . . . . . . 9 |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )
10	8, 9	syld3an1 1230	. . . . . . . 8 |- ( ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )
11		tfrcllemsucfn.1	. . . . . . . 8 |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }
12		tfrcllembacc.4	. . . . . . . . 9 |- ( ph -> D e. X )
13	12	ad2antrr 475	. . . . . . . 8 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> D e. X )
14		simplr 500	. . . . . . . 8 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> z e. D )
15		tfrcllembacc.u	. . . . . . . . . 10 |- ( ( ph /\ x e. U. X ) -> suc x e. X )
16	15	adantlr 464	. . . . . . . . 9 |- ( ( ( ph /\ z e. D ) /\ x e. U. X ) -> suc x e. X )
17	16	adantlr 464	. . . . . . . 8 |- ( ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) /\ x e. U. X ) -> suc x e. X )
18		simpr1 955	. . . . . . . 8 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> g : z --> S )
19		simpr2 956	. . . . . . . 8 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> g e. A )
20	3, 5, 7, 10, 11, 13, 14, 17, 18, 19	tfrcllemsucaccv 6181	. . . . . . 7 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> ( g u. { <. z , ( G ` g ) >. } ) e. A )
21	2, 20	eqeltrd 2176	. . . . . 6 |- ( ( ( ph /\ z e. D ) /\ ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) ) -> h e. A )
22	21	ex 114	. . . . 5 |- ( ( ph /\ z e. D ) -> ( ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) -> h e. A ) )
23	22	exlimdv 1758	. . . 4 |- ( ( ph /\ z e. D ) -> ( E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) -> h e. A ) )
24	23	rexlimdva 2508	. . 3 |- ( ph -> ( E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) -> h e. A ) )
25	24	abssdv 3118	. 2 |- ( ph -> { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) } C_ A )
26	1, 25	syl5eqss 3093	1 |- ( ph -> B C_ A )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 930   = wceq 1299   E.wex 1436   e. wcel 1448   {cab 2086   A.wral 2375   E.wrex 2376   u. cun 3019   C_ wss 3021   {csn 3474   <.cop 3477   U.cuni 3683   Ord word 4222   suc csuc 4225   |` cres 4479   Fun wfun 5053   -->wf 5055   ` cfv 5059  recscrecs 6131

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-ral 2380  df-rex 2381  df-v 2643  df-sbc 2863  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-tr 3967  df-id 4153  df-iord 4226  df-on 4228  df-suc 4231  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067

This theorem is referenced by:  tfrcllembfn  6184  tfrcllemubacc  6186