Metamath Proof Explorer

Theorem axlowdimlem15

Description: Lemma for axlowdim . Set up a one-to-one function of points. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypothesis axlowdimlem15.1 
|- F = ( i e. ( 1 ... ( N - 1 ) ) |-> if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) )
Assertion axlowdimlem15 
|- ( N e. ( ZZ>= ` 3 ) -> F : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem15.1 
 |-  F = ( i e. ( 1 ... ( N - 1 ) ) |-> if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) )
2 eqid 
 |-  ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
3 2 axlowdimlem7 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. ( EE ` N ) )
4 3 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 1 ... ( N - 1 ) ) ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. ( EE ` N ) )
5 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
6 eqid 
 |-  ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
7 6 axlowdimlem10 
 |-  ( ( N e. NN /\ i e. ( 1 ... ( N - 1 ) ) ) -> ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) e. ( EE ` N ) )
8 5 7 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 1 ... ( N - 1 ) ) ) -> ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) e. ( EE ` N ) )
9 4 8 ifcld 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 1 ... ( N - 1 ) ) ) -> if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) e. ( EE ` N ) )
10 9 1 fmptd 
 |-  ( N e. ( ZZ>= ` 3 ) -> F : ( 1 ... ( N - 1 ) ) --> ( EE ` N ) )
11 eqeq1 
 |-  ( i = j -> ( i = 1 <-> j = 1 ) )
12 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
13 12 opeq1d 
 |-  ( i = j -> <. ( i + 1 ) , 1 >. = <. ( j + 1 ) , 1 >. )
14 13 sneqd 
 |-  ( i = j -> { <. ( i + 1 ) , 1 >. } = { <. ( j + 1 ) , 1 >. } )
15 12 sneqd 
 |-  ( i = j -> { ( i + 1 ) } = { ( j + 1 ) } )
16 15 difeq2d 
 |-  ( i = j -> ( ( 1 ... N ) \ { ( i + 1 ) } ) = ( ( 1 ... N ) \ { ( j + 1 ) } ) )
17 16 xpeq1d 
 |-  ( i = j -> ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) )
18 14 17 uneq12d 
 |-  ( i = j -> ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) )
19 11 18 ifbieq2d 
 |-  ( i = j -> if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) = if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) )
20 snex 
 |-  { <. 3 , -u 1 >. } e. _V
21 ovex 
 |-  ( 1 ... N ) e. _V
22 21 difexi 
 |-  ( ( 1 ... N ) \ { 3 } ) e. _V
23 snex 
 |-  { 0 } e. _V
24 22 23 xpex 
 |-  ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) e. _V
25 20 24 unex 
 |-  ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. _V
26 snex 
 |-  { <. ( j + 1 ) , 1 >. } e. _V
27 21 difexi 
 |-  ( ( 1 ... N ) \ { ( j + 1 ) } ) e. _V
28 27 23 xpex 
 |-  ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) e. _V
29 26 28 unex 
 |-  ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) e. _V
30 25 29 ifex 
 |-  if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) e. _V
31 19 1 30 fvmpt 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( F ` j ) = if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) )
32 eqeq1 
 |-  ( i = k -> ( i = 1 <-> k = 1 ) )
33 oveq1 
 |-  ( i = k -> ( i + 1 ) = ( k + 1 ) )
34 33 opeq1d 
 |-  ( i = k -> <. ( i + 1 ) , 1 >. = <. ( k + 1 ) , 1 >. )
35 34 sneqd 
 |-  ( i = k -> { <. ( i + 1 ) , 1 >. } = { <. ( k + 1 ) , 1 >. } )
36 33 sneqd 
 |-  ( i = k -> { ( i + 1 ) } = { ( k + 1 ) } )
37 36 difeq2d 
 |-  ( i = k -> ( ( 1 ... N ) \ { ( i + 1 ) } ) = ( ( 1 ... N ) \ { ( k + 1 ) } ) )
38 37 xpeq1d 
 |-  ( i = k -> ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) )
39 35 38 uneq12d 
 |-  ( i = k -> ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) )
40 32 39 ifbieq2d 
 |-  ( i = k -> if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) )
41 snex 
 |-  { <. ( k + 1 ) , 1 >. } e. _V
42 21 difexi 
 |-  ( ( 1 ... N ) \ { ( k + 1 ) } ) e. _V
43 42 23 xpex 
 |-  ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) e. _V
44 41 43 unex 
 |-  ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) e. _V
45 25 44 ifex 
 |-  if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) e. _V
46 40 1 45 fvmpt 
 |-  ( k e. ( 1 ... ( N - 1 ) ) -> ( F ` k ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) )
47 31 46 eqeqan12d 
 |-  ( ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( F ` j ) = ( F ` k ) <-> if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) )
48 47 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( F ` j ) = ( F ` k ) <-> if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) )
49 eqtr3 
 |-  ( ( j = 1 /\ k = 1 ) -> j = k )
50 49 2a1d 
 |-  ( ( j = 1 /\ k = 1 ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) ) )
51 eqid 
 |-  ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) )
52 2 51 axlowdimlem13 
 |-  ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) =/= ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) )
53 52 neneqd 
 |-  ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> -. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) )
54 53 pm2.21d 
 |-  ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) )
55 54 adantrl 
 |-  ( ( N e. NN /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) )
56 5 55 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) )
57 iftrue 
 |-  ( j = 1 -> if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) )
58 iffalse 
 |-  ( -. k = 1 -> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) )
59 57 58 eqeqan12d 
 |-  ( ( j = 1 /\ -. k = 1 ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) <-> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) )
60 59 imbi1d 
 |-  ( ( j = 1 /\ -. k = 1 ) -> ( ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) <-> ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) ) )
61 56 60 syl5ibr 
 |-  ( ( j = 1 /\ -. k = 1 ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) ) )
62 eqid 
 |-  ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) )
63 2 62 axlowdimlem13 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) =/= ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) )
64 63 necomd 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) =/= ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) )
65 64 neneqd 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> -. ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) )
66 65 pm2.21d 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) -> j = k ) )
67 5 66 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) -> j = k ) )
68 67 adantrr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) -> j = k ) )
69 iffalse 
 |-  ( -. j = 1 -> if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) )
70 iftrue 
 |-  ( k = 1 -> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) )
71 69 70 eqeqan12d 
 |-  ( ( -. j = 1 /\ k = 1 ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) <-> ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) ) )
72 71 imbi1d 
 |-  ( ( -. j = 1 /\ k = 1 ) -> ( ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) <-> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) -> j = k ) ) )
73 68 72 syl5ibr 
 |-  ( ( -. j = 1 /\ k = 1 ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) ) )
74 62 51 axlowdimlem14 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) )
75 74 3expb 
 |-  ( ( N e. NN /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) )
76 5 75 sylan 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) )
77 69 58 eqeqan12d 
 |-  ( ( -. j = 1 /\ -. k = 1 ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) <-> ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) )
78 77 imbi1d 
 |-  ( ( -. j = 1 /\ -. k = 1 ) -> ( ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) <-> ( ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) = ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) -> j = k ) ) )
79 76 78 syl5ibr 
 |-  ( ( -. j = 1 /\ -. k = 1 ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) ) )
80 50 61 73 79 4cases 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( if ( j = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( j + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( j + 1 ) } ) X. { 0 } ) ) ) = if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) -> j = k ) )
81 48 80 sylbid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( j e. ( 1 ... ( N - 1 ) ) /\ k e. ( 1 ... ( N - 1 ) ) ) ) -> ( ( F ` j ) = ( F ` k ) -> j = k ) )
82 81 ralrimivva 
 |-  ( N e. ( ZZ>= ` 3 ) -> A. j e. ( 1 ... ( N - 1 ) ) A. k e. ( 1 ... ( N - 1 ) ) ( ( F ` j ) = ( F ` k ) -> j = k ) )
83 dff13 
 |-  ( F : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) <-> ( F : ( 1 ... ( N - 1 ) ) --> ( EE ` N ) /\ A. j e. ( 1 ... ( N - 1 ) ) A. k e. ( 1 ... ( N - 1 ) ) ( ( F ` j ) = ( F ` k ) -> j = k ) ) )
84 10 82 83 sylanbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> F : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) )