Step |
Hyp |
Ref |
Expression |
1 |
|
satf0 |
|- ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) |` suc _om ) |
2 |
1
|
fveq1i |
|- ( ( (/) Sat (/) ) ` N ) = ( ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) |` suc _om ) ` N ) |
3 |
|
fvres |
|- ( N e. suc _om -> ( ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) |` suc _om ) ` N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) |
4 |
2 3
|
syl5eq |
|- ( N e. suc _om -> ( ( (/) Sat (/) ) ` N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) |