Metamath Proof Explorer

Theorem axlowdimlem8

Description: Lemma for axlowdim . Calculate the value of P at three. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypothesis axlowdimlem7.1 
|- P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
Assertion axlowdimlem8 
|- ( P ` 3 ) = -u 1

Proof

Step Hyp Ref Expression
1 axlowdimlem7.1 
 |-  P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
2 1 fveq1i 
 |-  ( P ` 3 ) = ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` 3 )
3 3ex 
 |-  3 e. _V
4 negex 
 |-  -u 1 e. _V
5 3 4 fnsn 
 |-  { <. 3 , -u 1 >. } Fn { 3 }
6 c0ex 
 |-  0 e. _V
7 6 fconst 
 |-  ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> { 0 }
8 ffn 
 |-  ( ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) : ( ( 1 ... N ) \ { 3 } ) --> { 0 } -> ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { 3 } ) )
9 7 8 ax-mp 
 |-  ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { 3 } )
10 disjdif 
 |-  ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/)
11 3 snid 
 |-  3 e. { 3 }
12 10 11 pm3.2i 
 |-  ( ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/) /\ 3 e. { 3 } )
13 fvun1 
 |-  ( ( { <. 3 , -u 1 >. } Fn { 3 } /\ ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { 3 } ) /\ ( ( { 3 } i^i ( ( 1 ... N ) \ { 3 } ) ) = (/) /\ 3 e. { 3 } ) ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` 3 ) = ( { <. 3 , -u 1 >. } ` 3 ) )
14 5 9 12 13 mp3an 
 |-  ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ` 3 ) = ( { <. 3 , -u 1 >. } ` 3 )
15 3 4 fvsn 
 |-  ( { <. 3 , -u 1 >. } ` 3 ) = -u 1
16 2 14 15 3eqtri 
 |-  ( P ` 3 ) = -u 1