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