Theorem csbwrecsg 33173

Description: Move class substitution in and out of the well-founded recursive function generator . (Contributed by ML, 25-Oct-2020.)

Assertion

Ref	Expression
csbwrecsg	|- ( A e. V -> [_ A / x ]_wrecs ( R , D , F ) = wrecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) )

Proof of Theorem csbwrecsg

Dummy variables f y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbuni 4466	. . 3 |- [_ A / x ]_ U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) } = U. [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) }
2		csbab 4008	. . . . 5 |- [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) } = { f | [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) }
3		sbcex2 3486	. . . . . . 7 |- ( [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) <-> E. z [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) )
4		sbc3an 3494	. . . . . . . . 9 |- ( [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) <-> ( [. A / x ]. f Fn z /\ [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ [. A / x ]. A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) )
5		sbcg 3503	. . . . . . . . . 10 |- ( A e. V -> ( [. A / x ]. f Fn z <-> f Fn z ) )
6		sbcan 3478	. . . . . . . . . . 11 |- ( [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) <-> ( [. A / x ]. z C_ D /\ [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z ) )
7		sbcssg 4085	. . . . . . . . . . . . 13 |- ( A e. V -> ( [. A / x ]. z C_ D <-> [_ A / x ]_ z C_ [_ A / x ]_ D ) )
8		csbconstg 3546	. . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ z = z )
9	8	sseq1d 3632	. . . . . . . . . . . . 13 |- ( A e. V -> ( [_ A / x ]_ z C_ [_ A / x ]_ D <-> z C_ [_ A / x ]_ D ) )
10	7, 9	bitrd 268	. . . . . . . . . . . 12 |- ( A e. V -> ( [. A / x ]. z C_ D <-> z C_ [_ A / x ]_ D ) )
11		sbcralg 3513	. . . . . . . . . . . . 13 |- ( A e. V -> ( [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z <-> A. y e. z [. A / x ]. Pred ( R , D , y ) C_ z ) )
12		sbcssg 4085	. . . . . . . . . . . . . . 15 |- ( A e. V -> ( [. A / x ]. Pred ( R , D , y ) C_ z <-> [_ A / x ]_ Pred ( R , D , y ) C_ [_ A / x ]_ z ) )
13	8	sseq2d 3633	. . . . . . . . . . . . . . 15 |- ( A e. V -> ( [_ A / x ]_ Pred ( R , D , y ) C_ [_ A / x ]_ z <-> [_ A / x ]_ Pred ( R , D , y ) C_ z ) )
14		csbpredg 33172	. . . . . . . . . . . . . . . . 17 |- ( A e. V -> [_ A / x ]_ Pred ( R , D , y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) )
15		csbconstg 3546	. . . . . . . . . . . . . . . . . 18 |- ( A e. V -> [_ A / x ]_ y = y )
16		predeq3 5684	. . . . . . . . . . . . . . . . . 18 |- ( [_ A / x ]_ y = y -> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
17	15, 16	syl 17	. . . . . . . . . . . . . . . . 17 |- ( A e. V -> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
18	14, 17	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( A e. V -> [_ A / x ]_ Pred ( R , D , y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
19	18	sseq1d 3632	. . . . . . . . . . . . . . 15 |- ( A e. V -> ( [_ A / x ]_ Pred ( R , D , y ) C_ z <-> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
20	12, 13, 19	3bitrd 294	. . . . . . . . . . . . . 14 |- ( A e. V -> ( [. A / x ]. Pred ( R , D , y ) C_ z <-> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
21	20	ralbidv 2986	. . . . . . . . . . . . 13 |- ( A e. V -> ( A. y e. z [. A / x ]. Pred ( R , D , y ) C_ z <-> A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
22	11, 21	bitrd 268	. . . . . . . . . . . 12 |- ( A e. V -> ( [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z <-> A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
23	10, 22	anbi12d 747	. . . . . . . . . . 11 |- ( A e. V -> ( ( [. A / x ]. z C_ D /\ [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z ) <-> ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) ) )
24	6, 23	syl5bb 272	. . . . . . . . . 10 |- ( A e. V -> ( [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) <-> ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) ) )
25		sbcralg 3513	. . . . . . . . . . 11 |- ( A e. V -> ( [. A / x ]. A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) )
26		sbceqg 3984	. . . . . . . . . . . . 13 |- ( A e. V -> ( [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> [_ A / x ]_ ( f ` y ) = [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) ) )
27		csbconstg 3546	. . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ ( f ` y ) = ( f ` y ) )
28		csbfv12 6231	. . . . . . . . . . . . . . 15 |- [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ F ` [_ A / x ]_ ( f |` Pred ( R , D , y ) ) )
29		csbres 5399	. . . . . . . . . . . . . . . . 17 |- [_ A / x ]_ ( f |` Pred ( R , D , y ) ) = ( [_ A / x ]_ f |` [_ A / x ]_ Pred ( R , D , y ) )
30		csbconstg 3546	. . . . . . . . . . . . . . . . . 18 |- ( A e. V -> [_ A / x ]_ f = f )
31	30, 18	reseq12d 5397	. . . . . . . . . . . . . . . . 17 |- ( A e. V -> ( [_ A / x ]_ f |` [_ A / x ]_ Pred ( R , D , y ) ) = ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) )
32	29, 31	syl5eq 2668	. . . . . . . . . . . . . . . 16 |- ( A e. V -> [_ A / x ]_ ( f |` Pred ( R , D , y ) ) = ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) )
33	32	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( A e. V -> ( [_ A / x ]_ F ` [_ A / x ]_ ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) )
34	28, 33	syl5eq 2668	. . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) )
35	27, 34	eqeq12d 2637	. . . . . . . . . . . . 13 |- ( A e. V -> ( [_ A / x ]_ ( f ` y ) = [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) <-> ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
36	26, 35	bitrd 268	. . . . . . . . . . . 12 |- ( A e. V -> ( [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
37	36	ralbidv 2986	. . . . . . . . . . 11 |- ( A e. V -> ( A. y e. z [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
38	25, 37	bitrd 268	. . . . . . . . . 10 |- ( A e. V -> ( [. A / x ]. A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
39	5, 24, 38	3anbi123d 1399	. . . . . . . . 9 |- ( A e. V -> ( ( [. A / x ]. f Fn z /\ [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ [. A / x ]. A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) <-> ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
40	4, 39	syl5bb 272	. . . . . . . 8 |- ( A e. V -> ( [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) <-> ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
41	40	exbidv 1850	. . . . . . 7 |- ( A e. V -> ( E. z [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) <-> E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
42	3, 41	syl5bb 272	. . . . . 6 |- ( A e. V -> ( [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) <-> E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
43	42	abbidv 2741	. . . . 5 |- ( A e. V -> { f | [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) } = { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
44	2, 43	syl5eq 2668	. . . 4 |- ( A e. V -> [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) } = { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
45	44	unieqd 4446	. . 3 |- ( A e. V -> U. [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) } = U. { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
46	1, 45	syl5eq 2668	. 2 |- ( A e. V -> [_ A / x ]_ U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) } = U. { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
47		df-wrecs 7407	. . 3 |- wrecs ( R , D , F ) = U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) }
48	47	csbeq2i 3993	. 2 |- [_ A / x ]_wrecs ( R , D , F ) = [_ A / x ]_ U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) }
49		df-wrecs 7407	. 2 |- wrecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) = U. { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) }
50	46, 48, 49	3eqtr4g 2681	1 |- ( A e. V -> [_ A / x ]_wrecs ( R , D , F ) = wrecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   A.wral 2912   [.wsbc 3435   [_csb 3533   C_ wss 3574   U.cuni 4436   |` cres 5116   Predcpred 5679   Fn wfn 5883   ` cfv 5888  wrecscwrecs 7406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-iota 5851  df-fv 5896  df-wrecs 7407

This theorem is referenced by:  csbrecsg  33174