Metamath Proof Explorer


Theorem poimirlem17

Description: Lemma for poimir establishing existence for poimirlem18 . (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0
|- ( ph -> N e. NN )
poimirlem22.s
|- S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
poimirlem22.1
|- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
poimirlem22.2
|- ( ph -> T e. S )
poimirlem18.3
|- ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
poimirlem18.4
|- ( ph -> ( 2nd ` T ) = 0 )
Assertion poimirlem17
|- ( ph -> E. z e. S z =/= T )

Proof

Step Hyp Ref Expression
1 poimir.0
 |-  ( ph -> N e. NN )
2 poimirlem22.s
 |-  S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
3 poimirlem22.1
 |-  ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
4 poimirlem22.2
 |-  ( ph -> T e. S )
5 poimirlem18.3
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
6 poimirlem18.4
 |-  ( ph -> ( 2nd ` T ) = 0 )
7 1 2 3 4 5 6 poimirlem16
 |-  ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
8 elfznn0
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y e. NN0 )
9 8 nn0red
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
10 9 adantl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. RR )
11 1 nnzd
 |-  ( ph -> N e. ZZ )
12 peano2zm
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
13 11 12 syl
 |-  ( ph -> ( N - 1 ) e. ZZ )
14 13 zred
 |-  ( ph -> ( N - 1 ) e. RR )
15 14 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
16 1 nnred
 |-  ( ph -> N e. RR )
17 16 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. RR )
18 elfzle2
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y <_ ( N - 1 ) )
19 18 adantl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y <_ ( N - 1 ) )
20 16 ltm1d
 |-  ( ph -> ( N - 1 ) < N )
21 20 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
22 10 15 17 19 21 lelttrd
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y < N )
23 22 adantlr
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> y < N )
24 fveq2
 |-  ( t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( 2nd ` t ) = ( 2nd ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) )
25 opex
 |-  <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. e. _V
26 op2ndg
 |-  ( ( <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. e. _V /\ N e. NN ) -> ( 2nd ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) = N )
27 25 1 26 sylancr
 |-  ( ph -> ( 2nd ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) = N )
28 24 27 sylan9eqr
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( 2nd ` t ) = N )
29 28 adantr
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` t ) = N )
30 23 29 breqtrrd
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> y < ( 2nd ` t ) )
31 30 iftrued
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = y )
32 31 csbeq1d
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ y / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
33 vex
 |-  y e. _V
34 oveq2
 |-  ( j = y -> ( 1 ... j ) = ( 1 ... y ) )
35 34 imaeq2d
 |-  ( j = y -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) )
36 35 xpeq1d
 |-  ( j = y -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) )
37 oveq1
 |-  ( j = y -> ( j + 1 ) = ( y + 1 ) )
38 37 oveq1d
 |-  ( j = y -> ( ( j + 1 ) ... N ) = ( ( y + 1 ) ... N ) )
39 38 imaeq2d
 |-  ( j = y -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) )
40 39 xpeq1d
 |-  ( j = y -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
41 36 40 uneq12d
 |-  ( j = y -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) )
42 41 oveq2d
 |-  ( j = y -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
43 33 42 csbie
 |-  [_ y / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) )
44 2fveq3
 |-  ( t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) ) )
45 op1stg
 |-  ( ( <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. e. _V /\ N e. NN ) -> ( 1st ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) = <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. )
46 25 1 45 sylancr
 |-  ( ph -> ( 1st ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) = <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. )
47 46 fveq2d
 |-  ( ph -> ( 1st ` ( 1st ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) ) = ( 1st ` <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. ) )
48 ovex
 |-  ( 1 ... N ) e. _V
49 48 mptex
 |-  ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) e. _V
50 fvex
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
51 48 mptex
 |-  ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) e. _V
52 50 51 coex
 |-  ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) e. _V
53 49 52 op1st
 |-  ( 1st ` <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) )
54 47 53 eqtrdi
 |-  ( ph -> ( 1st ` ( 1st ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) )
55 44 54 sylan9eqr
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( 1st ` ( 1st ` t ) ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) )
56 fveq2
 |-  ( t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( 1st ` t ) = ( 1st ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) )
57 56 46 sylan9eqr
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( 1st ` t ) = <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. )
58 57 fveq2d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. ) )
59 49 52 op2nd
 |-  ( 2nd ` <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. ) = ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) )
60 58 59 eqtrdi
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) )
61 60 imaeq1d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) )
62 61 xpeq1d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) )
63 60 imaeq1d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) )
64 63 xpeq1d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
65 62 64 uneq12d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) )
66 55 65 oveq12d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
67 43 66 syl5eq
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> [_ y / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
68 67 adantr
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ y / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
69 32 68 eqtrd
 |-  ( ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
70 69 mpteq2dva
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
71 70 eqeq2d
 |-  ( ( ph /\ t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
72 71 ex
 |-  ( ph -> ( t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) ) )
73 72 alrimiv
 |-  ( ph -> A. t ( t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) ) )
74 oveq2
 |-  ( 1 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) )
75 74 eleq1d
 |-  ( 1 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) e. ( 0 ..^ K ) <-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) e. ( 0 ..^ K ) ) )
76 oveq2
 |-  ( 0 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 0 ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) )
77 76 eleq1d
 |-  ( 0 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 0 ) e. ( 0 ..^ K ) <-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) e. ( 0 ..^ K ) ) )
78 fveq2
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
79 78 oveq1d
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
80 79 adantl
 |-  ( ( ph /\ n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
81 elrabi
 |-  ( T e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
82 81 2 eleq2s
 |-  ( T e. S -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
83 xp1st
 |-  ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
84 4 82 83 3syl
 |-  ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
85 xp1st
 |-  ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
86 elmapi
 |-  ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
87 84 85 86 3syl
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
88 4 82 syl
 |-  ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
89 xp2nd
 |-  ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
90 88 83 89 3syl
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
91 f1oeq1
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
92 50 91 elab
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
93 90 92 sylib
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
94 f1of
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
95 93 94 syl
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
96 nnuz
 |-  NN = ( ZZ>= ` 1 )
97 1 96 eleqtrdi
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
98 eluzfz1
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
99 97 98 syl
 |-  ( ph -> 1 e. ( 1 ... N ) )
100 95 99 ffvelrnd
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) )
101 87 100 ffvelrnd
 |-  ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. ( 0 ..^ K ) )
102 elfzonn0
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. NN0 )
103 peano2nn0
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. NN0 -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. NN0 )
104 101 102 103 3syl
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. NN0 )
105 elfzo0
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. ( 0 ..^ K ) <-> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. NN0 /\ K e. NN /\ ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) < K ) )
106 101 105 sylib
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. NN0 /\ K e. NN /\ ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) < K ) )
107 106 simp2d
 |-  ( ph -> K e. NN )
108 104 nn0red
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. RR )
109 107 nnred
 |-  ( ph -> K e. RR )
110 elfzolt2
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) < K )
111 101 110 syl
 |-  ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) < K )
112 101 102 syl
 |-  ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. NN0 )
113 112 nn0zd
 |-  ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. ZZ )
114 107 nnzd
 |-  ( ph -> K e. ZZ )
115 zltp1le
 |-  ( ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) e. ZZ /\ K e. ZZ ) -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) < K <-> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) <_ K ) )
116 113 114 115 syl2anc
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) < K <-> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) <_ K ) )
117 111 116 mpbid
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) <_ K )
118 fvex
 |-  ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. _V
119 eleq1
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( n e. ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) )
120 119 anbi2d
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ph /\ n e. ( 1 ... N ) ) <-> ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) ) )
121 fveq2
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( p ` n ) = ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
122 121 neeq1d
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( p ` n ) =/= K <-> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K ) )
123 122 rexbidv
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( E. p e. ran F ( p ` n ) =/= K <-> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K ) )
124 120 123 imbi12d
 |-  ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K ) <-> ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) -> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K ) ) )
125 118 124 5 vtocl
 |-  ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) -> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K )
126 100 125 mpdan
 |-  ( ph -> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K )
127 fveq1
 |-  ( p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
128 87 ffnd
 |-  ( ph -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
129 128 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
130 1ex
 |-  1 e. _V
131 fnconstg
 |-  ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
132 130 131 ax-mp
 |-  ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) )
133 c0ex
 |-  0 e. _V
134 fnconstg
 |-  ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
135 133 134 ax-mp
 |-  ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) )
136 132 135 pm3.2i
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
137 dff1o3
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` T ) ) ) )
138 137 simprbi
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` T ) ) )
139 imain
 |-  ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
140 93 138 139 3syl
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
141 nn0p1nn
 |-  ( y e. NN0 -> ( y + 1 ) e. NN )
142 8 141 syl
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. NN )
143 142 nnred
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. RR )
144 143 ltp1d
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) < ( ( y + 1 ) + 1 ) )
145 fzdisj
 |-  ( ( y + 1 ) < ( ( y + 1 ) + 1 ) -> ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
146 145 imaeq2d
 |-  ( ( y + 1 ) < ( ( y + 1 ) + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
147 ima0
 |-  ( ( 2nd ` ( 1st ` T ) ) " (/) ) = (/)
148 146 147 eqtrdi
 |-  ( ( y + 1 ) < ( ( y + 1 ) + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
149 144 148 syl
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
150 140 149 sylan9req
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
151 fnun
 |-  ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
152 136 150 151 sylancr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
153 imaundi
 |-  ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
154 142 peano2nnd
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. NN )
155 154 96 eleqtrdi
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
156 1 nncnd
 |-  ( ph -> N e. CC )
157 npcan1
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
158 156 157 syl
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
159 158 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
160 elfzuz3
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` y ) )
161 eluzp1p1
 |-  ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
162 160 161 syl
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
163 162 adantl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
164 159 163 eqeltrrd
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( y + 1 ) ) )
165 fzsplit2
 |-  ( ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( y + 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
166 155 164 165 syl2an2
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
167 166 imaeq2d
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
168 f1ofo
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
169 foima
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
170 93 168 169 3syl
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
171 170 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
172 167 171 eqtr3d
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
173 153 172 eqtr3id
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
174 173 fneq2d
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
175 152 174 mpbid
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
176 48 a1i
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) e. _V )
177 inidm
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
178 eqidd
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
179 f1ofn
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
180 93 179 syl
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
181 180 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
182 fzss2
 |-  ( N e. ( ZZ>= ` ( y + 1 ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
183 164 182 syl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
184 142 96 eleqtrdi
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
185 eluzfz1
 |-  ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( y + 1 ) ) )
186 184 185 syl
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> 1 e. ( 1 ... ( y + 1 ) ) )
187 186 adantl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> 1 e. ( 1 ... ( y + 1 ) ) )
188 fnfvima
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) /\ 1 e. ( 1 ... ( y + 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
189 181 183 187 188 syl3anc
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
190 fvun1
 |-  ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
191 132 135 190 mp3an12
 |-  ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
192 150 189 191 syl2anc
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
193 130 fvconst2
 |-  ( ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
194 189 193 syl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
195 192 194 eqtrd
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
196 195 adantr
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
197 129 175 176 176 177 178 196 ofval
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
198 100 197 mpidan
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
199 127 198 sylan9eqr
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
200 199 adantllr
 |-  ( ( ( ( ph /\ p e. ran F ) /\ y e. ( 0 ... ( N - 1 ) ) ) /\ p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
201 fveq2
 |-  ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
202 201 breq2d
 |-  ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
203 202 ifbid
 |-  ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
204 2fveq3
 |-  ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
205 2fveq3
 |-  ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
206 205 imaeq1d
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
207 206 xpeq1d
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
208 205 imaeq1d
 |-  ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
209 208 xpeq1d
 |-  ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
210 207 209 uneq12d
 |-  ( t = T -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
211 204 210 oveq12d
 |-  ( t = T -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
212 203 211 csbeq12dv
 |-  ( t = T -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
213 212 mpteq2dv
 |-  ( t = T -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
214 213 eqeq2d
 |-  ( t = T -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
215 214 2 elrab2
 |-  ( T e. S <-> ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
216 215 simprbi
 |-  ( T e. S -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
217 4 216 syl
 |-  ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
218 217 rneqd
 |-  ( ph -> ran F = ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
219 218 eleq2d
 |-  ( ph -> ( p e. ran F <-> p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
220 eqid
 |-  ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
221 ovex
 |-  ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
222 221 csbex
 |-  [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
223 220 222 elrnmpti
 |-  ( p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> E. y e. ( 0 ... ( N - 1 ) ) p = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
224 219 223 bitrdi
 |-  ( ph -> ( p e. ran F <-> E. y e. ( 0 ... ( N - 1 ) ) p = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
225 6 adantr
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` T ) = 0 )
226 elfzle1
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> 0 <_ y )
227 226 adantl
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> 0 <_ y )
228 225 227 eqbrtrd
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` T ) <_ y )
229 0re
 |-  0 e. RR
230 6 229 eqeltrdi
 |-  ( ph -> ( 2nd ` T ) e. RR )
231 lenlt
 |-  ( ( ( 2nd ` T ) e. RR /\ y e. RR ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
232 230 9 231 syl2an
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
233 228 232 mpbid
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> -. y < ( 2nd ` T ) )
234 233 iffalsed
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = ( y + 1 ) )
235 234 csbeq1d
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
236 ovex
 |-  ( y + 1 ) e. _V
237 oveq2
 |-  ( j = ( y + 1 ) -> ( 1 ... j ) = ( 1 ... ( y + 1 ) ) )
238 237 imaeq2d
 |-  ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
239 238 xpeq1d
 |-  ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
240 oveq1
 |-  ( j = ( y + 1 ) -> ( j + 1 ) = ( ( y + 1 ) + 1 ) )
241 240 oveq1d
 |-  ( j = ( y + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( y + 1 ) + 1 ) ... N ) )
242 241 imaeq2d
 |-  ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
243 242 xpeq1d
 |-  ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
244 239 243 uneq12d
 |-  ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
245 244 oveq2d
 |-  ( j = ( y + 1 ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
246 236 245 csbie
 |-  [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
247 235 246 eqtrdi
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
248 247 eqeq2d
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( p = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) <-> p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
249 248 rexbidva
 |-  ( ph -> ( E. y e. ( 0 ... ( N - 1 ) ) p = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) <-> E. y e. ( 0 ... ( N - 1 ) ) p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
250 224 249 bitrd
 |-  ( ph -> ( p e. ran F <-> E. y e. ( 0 ... ( N - 1 ) ) p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
251 250 biimpa
 |-  ( ( ph /\ p e. ran F ) -> E. y e. ( 0 ... ( N - 1 ) ) p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
252 200 251 r19.29a
 |-  ( ( ph /\ p e. ran F ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
253 eqtr3
 |-  ( ( ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) /\ K = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = K )
254 253 ex
 |-  ( ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) -> ( K = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = K ) )
255 252 254 syl
 |-  ( ( ph /\ p e. ran F ) -> ( K = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = K ) )
256 255 necon3d
 |-  ( ( ph /\ p e. ran F ) -> ( ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K -> K =/= ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) ) )
257 256 rexlimdva
 |-  ( ph -> ( E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) =/= K -> K =/= ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) ) )
258 126 257 mpd
 |-  ( ph -> K =/= ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) )
259 108 109 117 258 leneltd
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) < K )
260 elfzo0
 |-  ( ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. ( 0 ..^ K ) <-> ( ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. NN0 /\ K e. NN /\ ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) < K ) )
261 104 107 259 260 syl3anbrc
 |-  ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. ( 0 ..^ K ) )
262 261 adantr
 |-  ( ( ph /\ n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) + 1 ) e. ( 0 ..^ K ) )
263 80 262 eqeltrd
 |-  ( ( ph /\ n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) e. ( 0 ..^ K ) )
264 263 adantlr
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 1 ) e. ( 0 ..^ K ) )
265 87 ffvelrnda
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) )
266 elfzonn0
 |-  ( ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
267 265 266 syl
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
268 267 nn0cnd
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. CC )
269 268 addid1d
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 0 ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
270 269 265 eqeltrd
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 0 ) e. ( 0 ..^ K ) )
271 270 adantr
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + 0 ) e. ( 0 ..^ K ) )
272 75 77 264 271 ifbothda
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) e. ( 0 ..^ K ) )
273 272 fmpttd
 |-  ( ph -> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
274 ovex
 |-  ( 0 ..^ K ) e. _V
275 274 48 elmap
 |-  ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
276 273 275 sylibr
 |-  ( ph -> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
277 simpr
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> n e. ( 1 ... ( N - 1 ) ) )
278 1z
 |-  1 e. ZZ
279 13 278 jctil
 |-  ( ph -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ ) )
280 elfzelz
 |-  ( n e. ( 1 ... ( N - 1 ) ) -> n e. ZZ )
281 280 278 jctir
 |-  ( n e. ( 1 ... ( N - 1 ) ) -> ( n e. ZZ /\ 1 e. ZZ ) )
282 fzaddel
 |-  ( ( ( 1 e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( n e. ZZ /\ 1 e. ZZ ) ) -> ( n e. ( 1 ... ( N - 1 ) ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
283 279 281 282 syl2an
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... ( N - 1 ) ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
284 277 283 mpbid
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) )
285 158 oveq2d
 |-  ( ph -> ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... N ) )
286 285 adantr
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... N ) )
287 284 286 eleqtrd
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( ( 1 + 1 ) ... N ) )
288 287 ralrimiva
 |-  ( ph -> A. n e. ( 1 ... ( N - 1 ) ) ( n + 1 ) e. ( ( 1 + 1 ) ... N ) )
289 simpr
 |-  ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> y e. ( ( 1 + 1 ) ... N ) )
290 peano2z
 |-  ( 1 e. ZZ -> ( 1 + 1 ) e. ZZ )
291 278 290 ax-mp
 |-  ( 1 + 1 ) e. ZZ
292 11 291 jctil
 |-  ( ph -> ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) )
293 elfzelz
 |-  ( y e. ( ( 1 + 1 ) ... N ) -> y e. ZZ )
294 293 278 jctir
 |-  ( y e. ( ( 1 + 1 ) ... N ) -> ( y e. ZZ /\ 1 e. ZZ ) )
295 fzsubel
 |-  ( ( ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ 1 e. ZZ ) ) -> ( y e. ( ( 1 + 1 ) ... N ) <-> ( y - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
296 292 294 295 syl2an
 |-  ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> ( y e. ( ( 1 + 1 ) ... N ) <-> ( y - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
297 289 296 mpbid
 |-  ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> ( y - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) )
298 ax-1cn
 |-  1 e. CC
299 298 298 pncan3oi
 |-  ( ( 1 + 1 ) - 1 ) = 1
300 299 oveq1i
 |-  ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
301 297 300 eleqtrdi
 |-  ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> ( y - 1 ) e. ( 1 ... ( N - 1 ) ) )
302 293 zcnd
 |-  ( y e. ( ( 1 + 1 ) ... N ) -> y e. CC )
303 elfznn
 |-  ( n e. ( 1 ... ( N - 1 ) ) -> n e. NN )
304 303 nncnd
 |-  ( n e. ( 1 ... ( N - 1 ) ) -> n e. CC )
305 subadd2
 |-  ( ( y e. CC /\ 1 e. CC /\ n e. CC ) -> ( ( y - 1 ) = n <-> ( n + 1 ) = y ) )
306 298 305 mp3an2
 |-  ( ( y e. CC /\ n e. CC ) -> ( ( y - 1 ) = n <-> ( n + 1 ) = y ) )
307 306 bicomd
 |-  ( ( y e. CC /\ n e. CC ) -> ( ( n + 1 ) = y <-> ( y - 1 ) = n ) )
308 eqcom
 |-  ( y = ( n + 1 ) <-> ( n + 1 ) = y )
309 eqcom
 |-  ( n = ( y - 1 ) <-> ( y - 1 ) = n )
310 307 308 309 3bitr4g
 |-  ( ( y e. CC /\ n e. CC ) -> ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
311 302 304 310 syl2an
 |-  ( ( y e. ( ( 1 + 1 ) ... N ) /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
312 311 ralrimiva
 |-  ( y e. ( ( 1 + 1 ) ... N ) -> A. n e. ( 1 ... ( N - 1 ) ) ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
313 312 adantl
 |-  ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> A. n e. ( 1 ... ( N - 1 ) ) ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
314 reu6i
 |-  ( ( ( y - 1 ) e. ( 1 ... ( N - 1 ) ) /\ A. n e. ( 1 ... ( N - 1 ) ) ( y = ( n + 1 ) <-> n = ( y - 1 ) ) ) -> E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) )
315 301 313 314 syl2anc
 |-  ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) )
316 315 ralrimiva
 |-  ( ph -> A. y e. ( ( 1 + 1 ) ... N ) E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) )
317 eqid
 |-  ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) = ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) )
318 317 f1ompt
 |-  ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) <-> ( A. n e. ( 1 ... ( N - 1 ) ) ( n + 1 ) e. ( ( 1 + 1 ) ... N ) /\ A. y e. ( ( 1 + 1 ) ... N ) E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) ) )
319 288 316 318 sylanbrc
 |-  ( ph -> ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) )
320 f1osng
 |-  ( ( N e. NN /\ 1 e. _V ) -> { <. N , 1 >. } : { N } -1-1-onto-> { 1 } )
321 1 130 320 sylancl
 |-  ( ph -> { <. N , 1 >. } : { N } -1-1-onto-> { 1 } )
322 14 16 ltnled
 |-  ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
323 20 322 mpbid
 |-  ( ph -> -. N <_ ( N - 1 ) )
324 elfzle2
 |-  ( N e. ( 1 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
325 323 324 nsyl
 |-  ( ph -> -. N e. ( 1 ... ( N - 1 ) ) )
326 disjsn
 |-  ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) <-> -. N e. ( 1 ... ( N - 1 ) ) )
327 325 326 sylibr
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) )
328 1re
 |-  1 e. RR
329 328 ltp1i
 |-  1 < ( 1 + 1 )
330 291 zrei
 |-  ( 1 + 1 ) e. RR
331 328 330 ltnlei
 |-  ( 1 < ( 1 + 1 ) <-> -. ( 1 + 1 ) <_ 1 )
332 329 331 mpbi
 |-  -. ( 1 + 1 ) <_ 1
333 elfzle1
 |-  ( 1 e. ( ( 1 + 1 ) ... N ) -> ( 1 + 1 ) <_ 1 )
334 332 333 mto
 |-  -. 1 e. ( ( 1 + 1 ) ... N )
335 disjsn
 |-  ( ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) <-> -. 1 e. ( ( 1 + 1 ) ... N ) )
336 334 335 mpbir
 |-  ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/)
337 336 a1i
 |-  ( ph -> ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) )
338 f1oun
 |-  ( ( ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) /\ { <. N , 1 >. } : { N } -1-1-onto-> { 1 } ) /\ ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) /\ ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) ) ) -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
339 319 321 327 337 338 syl22anc
 |-  ( ph -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
340 130 a1i
 |-  ( ph -> 1 e. _V )
341 158 97 eqeltrd
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
342 uzid
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
343 peano2uz
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
344 13 342 343 3syl
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
345 158 344 eqeltrrd
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
346 fzsplit2
 |-  ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
347 341 345 346 syl2anc
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
348 158 oveq1d
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
349 fzsn
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
350 11 349 syl
 |-  ( ph -> ( N ... N ) = { N } )
351 348 350 eqtrd
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
352 351 uneq2d
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
353 347 352 eqtr2d
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) u. { N } ) = ( 1 ... N ) )
354 iftrue
 |-  ( n = N -> if ( n = N , 1 , ( n + 1 ) ) = 1 )
355 354 adantl
 |-  ( ( ph /\ n = N ) -> if ( n = N , 1 , ( n + 1 ) ) = 1 )
356 1 340 353 355 fmptapd
 |-  ( ph -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) u. { <. N , 1 >. } ) = ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) )
357 eleq1
 |-  ( n = N -> ( n e. ( 1 ... ( N - 1 ) ) <-> N e. ( 1 ... ( N - 1 ) ) ) )
358 357 notbid
 |-  ( n = N -> ( -. n e. ( 1 ... ( N - 1 ) ) <-> -. N e. ( 1 ... ( N - 1 ) ) ) )
359 325 358 syl5ibrcom
 |-  ( ph -> ( n = N -> -. n e. ( 1 ... ( N - 1 ) ) ) )
360 359 necon2ad
 |-  ( ph -> ( n e. ( 1 ... ( N - 1 ) ) -> n =/= N ) )
361 360 imp
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> n =/= N )
362 ifnefalse
 |-  ( n =/= N -> if ( n = N , 1 , ( n + 1 ) ) = ( n + 1 ) )
363 361 362 syl
 |-  ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> if ( n = N , 1 , ( n + 1 ) ) = ( n + 1 ) )
364 363 mpteq2dva
 |-  ( ph -> ( n e. ( 1 ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) )
365 364 uneq1d
 |-  ( ph -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) u. { <. N , 1 >. } ) = ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) )
366 356 365 eqtr3d
 |-  ( ph -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) )
367 347 352 eqtrd
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
368 uzid
 |-  ( 1 e. ZZ -> 1 e. ( ZZ>= ` 1 ) )
369 peano2uz
 |-  ( 1 e. ( ZZ>= ` 1 ) -> ( 1 + 1 ) e. ( ZZ>= ` 1 ) )
370 278 368 369 mp2b
 |-  ( 1 + 1 ) e. ( ZZ>= ` 1 )
371 fzsplit2
 |-  ( ( ( 1 + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` 1 ) ) -> ( 1 ... N ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) )
372 370 97 371 sylancr
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) )
373 fzsn
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
374 278 373 ax-mp
 |-  ( 1 ... 1 ) = { 1 }
375 374 uneq1i
 |-  ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) )
376 375 equncomi
 |-  ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } )
377 372 376 eqtrdi
 |-  ( ph -> ( 1 ... N ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
378 366 367 377 f1oeq123d
 |-  ( ph -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) ) )
379 339 378 mpbird
 |-  ( ph -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
380 f1oco
 |-  ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
381 93 379 380 syl2anc
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
382 f1oeq1
 |-  ( f = ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
383 52 382 elab
 |-  ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
384 381 383 sylibr
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
385 276 384 opelxpd
 |-  ( ph -> <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
386 1 nnnn0d
 |-  ( ph -> N e. NN0 )
387 nn0fz0
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
388 386 387 sylib
 |-  ( ph -> N e. ( 0 ... N ) )
389 385 388 opelxpd
 |-  ( ph -> <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
390 elrab3t
 |-  ( ( A. t ( t = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) ) /\ <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
391 73 389 390 syl2anc
 |-  ( ph -> ( <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
392 7 391 mpbird
 |-  ( ph -> <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } )
393 392 2 eleqtrrdi
 |-  ( ph -> <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. S )
394 fveqeq2
 |-  ( <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. = T -> ( ( 2nd ` <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. ) = N <-> ( 2nd ` T ) = N ) )
395 27 394 syl5ibcom
 |-  ( ph -> ( <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. = T -> ( 2nd ` T ) = N ) )
396 1 nnne0d
 |-  ( ph -> N =/= 0 )
397 neeq1
 |-  ( ( 2nd ` T ) = N -> ( ( 2nd ` T ) =/= 0 <-> N =/= 0 ) )
398 396 397 syl5ibrcom
 |-  ( ph -> ( ( 2nd ` T ) = N -> ( 2nd ` T ) =/= 0 ) )
399 395 398 syld
 |-  ( ph -> ( <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. = T -> ( 2nd ` T ) =/= 0 ) )
400 399 necon2d
 |-  ( ph -> ( ( 2nd ` T ) = 0 -> <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. =/= T ) )
401 6 400 mpd
 |-  ( ph -> <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. =/= T )
402 neeq1
 |-  ( z = <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. -> ( z =/= T <-> <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. =/= T ) )
403 402 rspcev
 |-  ( ( <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. e. S /\ <. <. ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) >. , N >. =/= T ) -> E. z e. S z =/= T )
404 393 401 403 syl2anc
 |-  ( ph -> E. z e. S z =/= T )