Metamath Proof Explorer

Theorem 1arympt1fv

Description: The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024)

Ref Expression
Hypothesis 1arympt1.f 
|- F = ( x e. ( X ^m { 0 } ) |-> ( A ` ( x ` 0 ) ) )
Assertion 1arympt1fv 
|- ( ( X e. V /\ B e. X ) -> ( F ` { <. 0 , B >. } ) = ( A ` B ) )

Proof

Step Hyp Ref Expression
1 1arympt1.f 
 |-  F = ( x e. ( X ^m { 0 } ) |-> ( A ` ( x ` 0 ) ) )
2 1 a1i 
 |-  ( ( X e. V /\ B e. X ) -> F = ( x e. ( X ^m { 0 } ) |-> ( A ` ( x ` 0 ) ) ) )
3 fveq1 
 |-  ( x = { <. 0 , B >. } -> ( x ` 0 ) = ( { <. 0 , B >. } ` 0 ) )
4 3 adantl 
 |-  ( ( ( X e. V /\ B e. X ) /\ x = { <. 0 , B >. } ) -> ( x ` 0 ) = ( { <. 0 , B >. } ` 0 ) )
5 c0ex 
 |-  0 e. _V
6 5 a1i 
 |-  ( X e. V -> 0 e. _V )
7 6 anim1i 
 |-  ( ( X e. V /\ B e. X ) -> ( 0 e. _V /\ B e. X ) )
8 7 adantr 
 |-  ( ( ( X e. V /\ B e. X ) /\ x = { <. 0 , B >. } ) -> ( 0 e. _V /\ B e. X ) )
9 fvsng 
 |-  ( ( 0 e. _V /\ B e. X ) -> ( { <. 0 , B >. } ` 0 ) = B )
10 8 9 syl 
 |-  ( ( ( X e. V /\ B e. X ) /\ x = { <. 0 , B >. } ) -> ( { <. 0 , B >. } ` 0 ) = B )
11 4 10 eqtrd 
 |-  ( ( ( X e. V /\ B e. X ) /\ x = { <. 0 , B >. } ) -> ( x ` 0 ) = B )
12 11 fveq2d 
 |-  ( ( ( X e. V /\ B e. X ) /\ x = { <. 0 , B >. } ) -> ( A ` ( x ` 0 ) ) = ( A ` B ) )
13 5 a1i 
 |-  ( ( X e. V /\ B e. X ) -> 0 e. _V )
14 simpr 
 |-  ( ( X e. V /\ B e. X ) -> B e. X )
15 13 14 fsnd 
 |-  ( ( X e. V /\ B e. X ) -> { <. 0 , B >. } : { 0 } --> X )
16 snex 
 |-  { 0 } e. _V
17 16 a1i 
 |-  ( B e. X -> { 0 } e. _V )
18 elmapg 
 |-  ( ( X e. V /\ { 0 } e. _V ) -> ( { <. 0 , B >. } e. ( X ^m { 0 } ) <-> { <. 0 , B >. } : { 0 } --> X ) )
19 17 18 sylan2 
 |-  ( ( X e. V /\ B e. X ) -> ( { <. 0 , B >. } e. ( X ^m { 0 } ) <-> { <. 0 , B >. } : { 0 } --> X ) )
20 15 19 mpbird 
 |-  ( ( X e. V /\ B e. X ) -> { <. 0 , B >. } e. ( X ^m { 0 } ) )
21 fvexd 
 |-  ( ( X e. V /\ B e. X ) -> ( A ` B ) e. _V )
22 2 12 20 21 fvmptd 
 |-  ( ( X e. V /\ B e. X ) -> ( F ` { <. 0 , B >. } ) = ( A ` B ) )