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