Metamath Proof Explorer


Theorem evl1fval1lem

Description: Lemma for evl1fval1 . (Contributed by AV, 11-Sep-2019)

Ref Expression
Hypotheses evl1fval1.q
|- Q = ( eval1 ` R )
evl1fval1.b
|- B = ( Base ` R )
Assertion evl1fval1lem
|- ( R e. V -> Q = ( R evalSub1 B ) )

Proof

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 ) )