| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evl1fval1.q |
|- Q = ( eval1 ` R ) |
| 2 |
|
evl1fval1.b |
|- B = ( Base ` R ) |
| 3 |
|
eqid |
|- ( eval1 ` R ) = ( eval1 ` R ) |
| 4 |
|
eqid |
|- ( 1o eval R ) = ( 1o eval R ) |
| 5 |
3 4 2
|
evl1fval |
|- ( eval1 ` R ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) ) |
| 6 |
1
|
a1i |
|- ( R e. V -> Q = ( eval1 ` R ) ) |
| 7 |
2
|
fvexi |
|- B e. _V |
| 8 |
7
|
pwid |
|- B e. ~P B |
| 9 |
|
eqid |
|- ( R evalSub1 B ) = ( R evalSub1 B ) |
| 10 |
|
eqid |
|- ( 1o evalSub R ) = ( 1o evalSub R ) |
| 11 |
9 10 2
|
evls1fval |
|- ( ( R e. V /\ B e. ~P B ) -> ( R evalSub1 B ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub R ) ` B ) ) ) |
| 12 |
8 11
|
mpan2 |
|- ( R e. V -> ( R evalSub1 B ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub R ) ` B ) ) ) |
| 13 |
4 2
|
evlval |
|- ( 1o eval R ) = ( ( 1o evalSub R ) ` B ) |
| 14 |
13
|
eqcomi |
|- ( ( 1o evalSub R ) ` B ) = ( 1o eval R ) |
| 15 |
14
|
coeq2i |
|- ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub R ) ` B ) ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) ) |
| 16 |
12 15
|
eqtrdi |
|- ( R e. V -> ( R evalSub1 B ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) ) ) |
| 17 |
5 6 16
|
3eqtr4a |
|- ( R e. V -> Q = ( R evalSub1 B ) ) |