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