Metamath Proof Explorer

Theorem 1fv

Description: A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Assertion 1fv 
|- ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 1 a1i 
 |-  ( N e. V -> 0 e. ZZ )
3 id 
 |-  ( N e. V -> N e. V )
4 2 3 fsnd 
 |-  ( N e. V -> { <. 0 , N >. } : { 0 } --> V )
5 fvsng 
 |-  ( ( 0 e. ZZ /\ N e. V ) -> ( { <. 0 , N >. } ` 0 ) = N )
6 1 5 mpan 
 |-  ( N e. V -> ( { <. 0 , N >. } ` 0 ) = N )
7 4 6 jca 
 |-  ( N e. V -> ( { <. 0 , N >. } : { 0 } --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) )
8 7 adantr 
 |-  ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( { <. 0 , N >. } : { 0 } --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) )
9 id 
 |-  ( P = { <. 0 , N >. } -> P = { <. 0 , N >. } )
10 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
11 10 a1i 
 |-  ( P = { <. 0 , N >. } -> ( 0 ... 0 ) = { 0 } )
12 9 11 feq12d 
 |-  ( P = { <. 0 , N >. } -> ( P : ( 0 ... 0 ) --> V <-> { <. 0 , N >. } : { 0 } --> V ) )
13 fveq1 
 |-  ( P = { <. 0 , N >. } -> ( P ` 0 ) = ( { <. 0 , N >. } ` 0 ) )
14 13 eqeq1d 
 |-  ( P = { <. 0 , N >. } -> ( ( P ` 0 ) = N <-> ( { <. 0 , N >. } ` 0 ) = N ) )
15 12 14 anbi12d 
 |-  ( P = { <. 0 , N >. } -> ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) <-> ( { <. 0 , N >. } : { 0 } --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) ) )
16 15 adantl 
 |-  ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) <-> ( { <. 0 , N >. } : { 0 } --> V /\ ( { <. 0 , N >. } ` 0 ) = N ) ) )
17 8 16 mpbird 
 |-  ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) )