Step |
Hyp |
Ref |
Expression |
1 |
|
df-finxp |
|- ( U ^^ N ) = { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } |
2 |
1
|
csbeq2i |
|- [_ A / x ]_ ( U ^^ N ) = [_ A / x ]_ { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } |
3 |
|
sbcan |
|- ( [. A / x ]. ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( [. A / x ]. N e. _om /\ [. A / x ]. (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) ) |
4 |
|
sbcel1g |
|- ( A e. V -> ( [. A / x ]. N e. _om <-> [_ A / x ]_ N e. _om ) ) |
5 |
|
sbceq2g |
|- ( A e. V -> ( [. A / x ]. (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = [_ A / x ]_ ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) ) |
6 |
|
csbfv12 |
|- [_ A / x ]_ ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) = ( [_ A / x ]_ rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` [_ A / x ]_ N ) |
7 |
|
csbrdgg |
|- ( A e. V -> [_ A / x ]_ rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) = rec ( [_ A / x ]_ ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , [_ A / x ]_ <. N , y >. ) ) |
8 |
|
csbmpo123 |
|- ( A e. V -> [_ A / x ]_ ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. [_ A / x ]_ _om , z e. [_ A / x ]_ _V |-> [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) ) |
9 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ _om = _om ) |
10 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ _V = _V ) |
11 |
|
csbif |
|- [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) = if ( [. A / x ]. ( n = 1o /\ z e. U ) , [_ A / x ]_ (/) , [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) |
12 |
|
sbcan |
|- ( [. A / x ]. ( n = 1o /\ z e. U ) <-> ( [. A / x ]. n = 1o /\ [. A / x ]. z e. U ) ) |
13 |
|
sbcg |
|- ( A e. V -> ( [. A / x ]. n = 1o <-> n = 1o ) ) |
14 |
|
sbcel12 |
|- ( [. A / x ]. z e. U <-> [_ A / x ]_ z e. [_ A / x ]_ U ) |
15 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ z = z ) |
16 |
15
|
eleq1d |
|- ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ U <-> z e. [_ A / x ]_ U ) ) |
17 |
14 16
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. z e. U <-> z e. [_ A / x ]_ U ) ) |
18 |
13 17
|
anbi12d |
|- ( A e. V -> ( ( [. A / x ]. n = 1o /\ [. A / x ]. z e. U ) <-> ( n = 1o /\ z e. [_ A / x ]_ U ) ) ) |
19 |
12 18
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. ( n = 1o /\ z e. U ) <-> ( n = 1o /\ z e. [_ A / x ]_ U ) ) ) |
20 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ (/) = (/) ) |
21 |
|
csbif |
|- [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) = if ( [. A / x ]. z e. ( _V X. U ) , [_ A / x ]_ <. U. n , ( 1st ` z ) >. , [_ A / x ]_ <. n , z >. ) |
22 |
|
sbcel12 |
|- ( [. A / x ]. z e. ( _V X. U ) <-> [_ A / x ]_ z e. [_ A / x ]_ ( _V X. U ) ) |
23 |
|
csbxp |
|- [_ A / x ]_ ( _V X. U ) = ( [_ A / x ]_ _V X. [_ A / x ]_ U ) |
24 |
10
|
xpeq1d |
|- ( A e. V -> ( [_ A / x ]_ _V X. [_ A / x ]_ U ) = ( _V X. [_ A / x ]_ U ) ) |
25 |
23 24
|
eqtrid |
|- ( A e. V -> [_ A / x ]_ ( _V X. U ) = ( _V X. [_ A / x ]_ U ) ) |
26 |
15 25
|
eleq12d |
|- ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ ( _V X. U ) <-> z e. ( _V X. [_ A / x ]_ U ) ) ) |
27 |
22 26
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. z e. ( _V X. U ) <-> z e. ( _V X. [_ A / x ]_ U ) ) ) |
28 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ <. U. n , ( 1st ` z ) >. = <. U. n , ( 1st ` z ) >. ) |
29 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ <. n , z >. = <. n , z >. ) |
30 |
27 28 29
|
ifbieq12d |
|- ( A e. V -> if ( [. A / x ]. z e. ( _V X. U ) , [_ A / x ]_ <. U. n , ( 1st ` z ) >. , [_ A / x ]_ <. n , z >. ) = if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) |
31 |
21 30
|
eqtrid |
|- ( A e. V -> [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) = if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) |
32 |
19 20 31
|
ifbieq12d |
|- ( A e. V -> if ( [. A / x ]. ( n = 1o /\ z e. U ) , [_ A / x ]_ (/) , [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) = if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) |
33 |
11 32
|
eqtrid |
|- ( A e. V -> [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) = if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) |
34 |
9 10 33
|
mpoeq123dv |
|- ( A e. V -> ( n e. [_ A / x ]_ _om , z e. [_ A / x ]_ _V |-> [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) ) |
35 |
8 34
|
eqtrd |
|- ( A e. V -> [_ A / x ]_ ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) ) |
36 |
|
csbopg |
|- ( A e. V -> [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , [_ A / x ]_ y >. ) |
37 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ y = y ) |
38 |
37
|
opeq2d |
|- ( A e. V -> <. [_ A / x ]_ N , [_ A / x ]_ y >. = <. [_ A / x ]_ N , y >. ) |
39 |
36 38
|
eqtrd |
|- ( A e. V -> [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , y >. ) |
40 |
|
rdgeq12 |
|- ( ( [_ A / x ]_ ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) /\ [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , y >. ) -> rec ( [_ A / x ]_ ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , [_ A / x ]_ <. N , y >. ) = rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ) |
41 |
35 39 40
|
syl2anc |
|- ( A e. V -> rec ( [_ A / x ]_ ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , [_ A / x ]_ <. N , y >. ) = rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ) |
42 |
7 41
|
eqtrd |
|- ( A e. V -> [_ A / x ]_ rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) = rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ) |
43 |
42
|
fveq1d |
|- ( A e. V -> ( [_ A / x ]_ rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` [_ A / x ]_ N ) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) |
44 |
6 43
|
eqtrid |
|- ( A e. V -> [_ A / x ]_ ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) |
45 |
44
|
eqeq2d |
|- ( A e. V -> ( (/) = [_ A / x ]_ ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) ) |
46 |
5 45
|
bitrd |
|- ( A e. V -> ( [. A / x ]. (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) ) |
47 |
4 46
|
anbi12d |
|- ( A e. V -> ( ( [. A / x ]. N e. _om /\ [. A / x ]. (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( [_ A / x ]_ N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) ) ) |
48 |
3 47
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( [_ A / x ]_ N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) ) ) |
49 |
48
|
abbidv |
|- ( A e. V -> { y | [. A / x ]. ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } = { y | ( [_ A / x ]_ N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) } ) |
50 |
|
csbab |
|- [_ A / x ]_ { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } = { y | [. A / x ]. ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } |
51 |
|
df-finxp |
|- ( [_ A / x ]_ U ^^ [_ A / x ]_ N ) = { y | ( [_ A / x ]_ N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) } |
52 |
49 50 51
|
3eqtr4g |
|- ( A e. V -> [_ A / x ]_ { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } = ( [_ A / x ]_ U ^^ [_ A / x ]_ N ) ) |
53 |
2 52
|
eqtrid |
|- ( A e. V -> [_ A / x ]_ ( U ^^ N ) = ( [_ A / x ]_ U ^^ [_ A / x ]_ N ) ) |