Metamath Proof Explorer

Theorem poimirlem9

Description: Lemma for poimir , establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (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 } ) ) ) ) }
poimirlem9.1 
|- ( ph -> T e. S )
poimirlem9.2 
|- ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
poimirlem9.3 
|- ( ph -> U e. S )
poimirlem9.4 
|- ( ph -> ( 2nd ` ( 1st ` U ) ) =/= ( 2nd ` ( 1st ` T ) ) )
Assertion poimirlem9 
|- ( ph -> ( 2nd ` ( 1st ` U ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )

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 poimirlem9.1 
 |-  ( ph -> T e. S )
4 poimirlem9.2 
 |-  ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
5 poimirlem9.3 
 |-  ( ph -> U e. S )
6 poimirlem9.4 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) =/= ( 2nd ` ( 1st ` T ) ) )
7 resundi 
 |-  ( ( 2nd ` ( 1st ` U ) ) |` ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
8 1 nncnd 
 |-  ( ph -> N e. CC )
9 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
10 8 9 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
11 1 nnzd 
 |-  ( ph -> N e. ZZ )
12 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
13 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
14 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
15 11 12 13 14 4syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
16 10 15 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
17 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
18 16 17 syl 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
19 18 4 sseldd 
 |-  ( ph -> ( 2nd ` T ) e. ( 1 ... N ) )
20 fzp1elp1 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
21 4 20 syl 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
22 10 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
23 21 22 eleqtrd 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) )
24 19 23 prssd 
 |-  ( ph -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) )
25 undif 
 |-  ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) <-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... N ) )
26 24 25 sylib 
 |-  ( ph -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... N ) )
27 26 reseq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` U ) ) |` ( 1 ... N ) ) )
28 elrabi 
 |-  ( U 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 } ) ) ) ) } -> U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
29 28 2 eleq2s 
 |-  ( U e. S -> U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
30 xp1st 
 |-  ( U e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
31 xp2nd 
 |-  ( ( 1st ` U ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
32 5 29 30 31 4syl 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
33 fvex 
 |-  ( 2nd ` ( 1st ` U ) ) e. _V
34 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` U ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
35 33 34 elab 
 |-  ( ( 2nd ` ( 1st ` U ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
36 32 35 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
37 f1ofn 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` U ) ) Fn ( 1 ... N ) )
38 fnresdm 
 |-  ( ( 2nd ` ( 1st ` U ) ) Fn ( 1 ... N ) -> ( ( 2nd ` ( 1st ` U ) ) |` ( 1 ... N ) ) = ( 2nd ` ( 1st ` U ) ) )
39 36 37 38 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( 1 ... N ) ) = ( 2nd ` ( 1st ` U ) ) )
40 27 39 eqtrd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( 2nd ` ( 1st ` U ) ) )
41 7 40 eqtr3id 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( 2nd ` ( 1st ` U ) ) )
42 2lt3 
 |-  2 < 3
43 2re 
 |-  2 e. RR
44 3re 
 |-  3 e. RR
45 43 44 ltnlei 
 |-  ( 2 < 3 <-> -. 3 <_ 2 )
46 42 45 mpbi 
 |-  -. 3 <_ 2
47 df-pr 
 |-  { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } u. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
48 47 coeq2i 
 |-  ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } u. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) )
49 coundi 
 |-  ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } u. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) )
50 48 49 eqtri 
 |-  ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) = ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) )
51 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 ) ) )
52 51 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 ) ) )
53 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 ) } ) )
54 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 ) } )
55 3 52 53 54 4syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
56 fvex 
 |-  ( 2nd ` ( 1st ` T ) ) e. _V
57 f1oeq1 
 |-  ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
58 56 57 elab 
 |-  ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
59 55 58 sylib 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
60 f1of1 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
61 59 60 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
62 23 snssd 
 |-  ( ph -> { ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) )
63 f1ores 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) /\ { ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } -1-1-onto-> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) )
64 61 62 63 syl2anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } -1-1-onto-> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) )
65 f1of 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } -1-1-onto-> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } --> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) )
66 64 65 syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } --> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) )
67 f1ofn 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
68 59 67 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
69 fnsnfv 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } = ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) )
70 68 23 69 syl2anc 
 |-  ( ph -> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } = ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) )
71 70 feq3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } <-> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } --> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) } ) ) )
72 66 71 mpbird 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
73 eqid 
 |-  { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } = { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. }
74 fvex 
 |-  ( 2nd ` T ) e. _V
75 ovex 
 |-  ( ( 2nd ` T ) + 1 ) e. _V
76 74 75 fsn 
 |-  ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } : { ( 2nd ` T ) } --> { ( ( 2nd ` T ) + 1 ) } <-> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } = { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } )
77 73 76 mpbir 
 |-  { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } : { ( 2nd ` T ) } --> { ( ( 2nd ` T ) + 1 ) }
78 fco2 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) : { ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } /\ { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } : { ( 2nd ` T ) } --> { ( ( 2nd ` T ) + 1 ) } ) -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) : { ( 2nd ` T ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
79 72 77 78 sylancl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) : { ( 2nd ` T ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
80 fvex 
 |-  ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) e. _V
81 80 fconst2 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) : { ( 2nd ` T ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } <-> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) = ( { ( 2nd ` T ) } X. { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } ) )
82 79 81 sylib 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) = ( { ( 2nd ` T ) } X. { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } ) )
83 74 80 xpsn 
 |-  ( { ( 2nd ` T ) } X. { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. }
84 82 83 eqtrdi 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
85 84 uneq1d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. } ) u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) = ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) )
86 50 85 eqtrid 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) = ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) )
87 elfznn 
 |-  ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) e. NN )
88 4 87 syl 
 |-  ( ph -> ( 2nd ` T ) e. NN )
89 88 nnred 
 |-  ( ph -> ( 2nd ` T ) e. RR )
90 89 ltp1d 
 |-  ( ph -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
91 89 90 ltned 
 |-  ( ph -> ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) )
92 91 necomd 
 |-  ( ph -> ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) )
93 f1veqaeq 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) /\ ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) /\ ( 2nd ` T ) e. ( 1 ... N ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) -> ( ( 2nd ` T ) + 1 ) = ( 2nd ` T ) ) )
94 61 23 19 93 syl12anc 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) -> ( ( 2nd ` T ) + 1 ) = ( 2nd ` T ) ) )
95 94 necon3d 
 |-  ( ph -> ( ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) -> ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) ) )
96 92 95 mpd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) )
97 96 neneqd 
 |-  ( ph -> -. ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) )
98 74 80 opth 
 |-  ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. <-> ( ( 2nd ` T ) = ( 2nd ` T ) /\ ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) ) )
99 98 simprbi 
 |-  ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. -> ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) = ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) )
100 97 99 nsyl 
 |-  ( ph -> -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. )
101 91 neneqd 
 |-  ( ph -> -. ( 2nd ` T ) = ( ( 2nd ` T ) + 1 ) )
102 74 80 opth1 
 |-  ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. -> ( 2nd ` T ) = ( ( 2nd ` T ) + 1 ) )
103 101 102 nsyl 
 |-  ( ph -> -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. )
104 opex 
 |-  <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. _V
105 104 snid 
 |-  <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. }
106 elun1 
 |-  ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } -> <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) )
107 105 106 ax-mp 
 |-  <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) )
108 eleq2 
 |-  ( ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } -> ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) <-> <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } ) )
109 107 108 mpbii 
 |-  ( ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } -> <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
110 104 elpr 
 |-  ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } <-> ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. \/ <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. ) )
111 oran 
 |-  ( ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. \/ <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. ) <-> -. ( -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. /\ -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. ) )
112 110 111 bitri 
 |-  ( <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. e. { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } <-> -. ( -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. /\ -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. ) )
113 109 112 sylib 
 |-  ( ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } -> -. ( -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. /\ -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. ) )
114 113 necon2ai 
 |-  ( ( -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. /\ -. <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. = <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
115 100 103 114 syl2anc 
 |-  ( ph -> ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } u. ( ( 2nd ` ( 1st ` T ) ) o. { <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
116 86 115 eqnetrd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
117 fnressn 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( 2nd ` T ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) } ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. } )
118 68 19 117 syl2anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) } ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. } )
119 fnressn 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) = { <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
120 68 23 119 syl2anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) = { <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
121 118 120 uneq12d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) ) = ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. } u. { <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } ) )
122 df-pr 
 |-  { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } = ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } )
123 122 reseq2i 
 |-  ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) |` ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) )
124 resundi 
 |-  ( ( 2nd ` ( 1st ` T ) ) |` ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) )
125 123 124 eqtri 
 |-  ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) } ) )
126 df-pr 
 |-  { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } = ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. } u. { <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
127 121 125 126 3eqtr4g 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } )
128 1 2 3 4 5 poimirlem8 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
129 uneq12 
 |-  ( ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
130 resundi 
 |-  ( ( 2nd ` ( 1st ` T ) ) |` ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
131 26 reseq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( 1 ... N ) ) )
132 fnresdm 
 |-  ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) |` ( 1 ... N ) ) = ( 2nd ` ( 1st ` T ) ) )
133 59 67 132 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` ( 1 ... N ) ) = ( 2nd ` ( 1st ` T ) ) )
134 131 133 eqtrd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( 2nd ` ( 1st ` T ) ) )
135 130 134 eqtr3id 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( 2nd ` ( 1st ` T ) ) )
136 41 135 eqeq12d 
 |-  ( ph -> ( ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) <-> ( 2nd ` ( 1st ` U ) ) = ( 2nd ` ( 1st ` T ) ) ) )
137 129 136 imbitrid 
 |-  ( ph -> ( ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) -> ( 2nd ` ( 1st ` U ) ) = ( 2nd ` ( 1st ` T ) ) ) )
138 128 137 mpan2d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( 2nd ` ( 1st ` U ) ) = ( 2nd ` ( 1st ` T ) ) ) )
139 138 necon3d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) =/= ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
140 6 139 mpd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
141 140 necomd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
142 127 141 eqnetrrd 
 |-  ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } =/= ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
143 prex 
 |-  { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } e. _V
144 56 143 coex 
 |-  ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) e. _V
145 prex 
 |-  { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } e. _V
146 33 resex 
 |-  ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. _V
147 hashtpg 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) e. _V /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } e. _V /\ ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. _V ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } =/= ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) <-> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 ) )
148 144 145 146 147 mp3an 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } =/= ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) <-> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 )
149 148 biimpi 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } =/= ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 )
150 149 3expia 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) =/= { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } =/= ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 ) )
151 116 142 150 syl2anc 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 ) )
152 prex 
 |-  { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } e. _V
153 prex 
 |-  { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. _V
154 152 153 mapval 
 |-  ( { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ^m { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } }
155 prfi 
 |-  { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } e. Fin
156 prfi 
 |-  { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. Fin
157 mapfi 
 |-  ( ( { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } e. Fin /\ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. Fin ) -> ( { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ^m { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. Fin )
158 155 156 157 mp2an 
 |-  ( { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ^m { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. Fin
159 154 158 eqeltrri 
 |-  { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } e. Fin
160 f1of 
 |-  ( f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } -> f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
161 160 ss2abi 
 |-  { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } }
162 ssfi 
 |-  ( ( { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } e. Fin /\ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) -> { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } e. Fin )
163 159 161 162 mp2an 
 |-  { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } e. Fin
164 23 19 prssd 
 |-  ( ph -> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } C_ ( 1 ... N ) )
165 f1ores 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) /\ { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } C_ ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) : { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -1-1-onto-> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) )
166 61 164 165 syl2anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) : { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -1-1-onto-> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) )
167 fnimapr 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) /\ ( 2nd ` T ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) = { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
168 68 23 19 167 syl3anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) = { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
169 168 f1oeq3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) : { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -1-1-onto-> ( ( 2nd ` ( 1st ` T ) ) " { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) <-> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) : { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
170 166 169 mpbid 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) : { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
171 f1oprg 
 |-  ( ( ( ( 2nd ` T ) e. _V /\ ( ( 2nd ` T ) + 1 ) e. _V ) /\ ( ( ( 2nd ` T ) + 1 ) e. _V /\ ( 2nd ` T ) e. _V ) ) -> ( ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) )
172 74 75 75 74 171 mp4an 
 |-  ( ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
173 91 92 172 syl2anc 
 |-  ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
174 f1oco 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) : { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } /\ { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
175 170 173 174 syl2anc 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
176 rnpropg 
 |-  ( ( ( 2nd ` T ) e. _V /\ ( ( 2nd ` T ) + 1 ) e. _V ) -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
177 74 75 176 mp2an 
 |-  ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) }
178 177 eqimssi 
 |-  ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } C_ { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) }
179 cores 
 |-  ( ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } C_ { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -> ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) = ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) )
180 f1oeq1 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) = ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } <-> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
181 178 179 180 mp2b 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) |` { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } <-> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
182 175 181 sylib 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
183 96 necomd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) )
184 fvex 
 |-  ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) e. _V
185 f1oprg 
 |-  ( ( ( ( 2nd ` T ) e. _V /\ ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) e. _V ) /\ ( ( ( 2nd ` T ) + 1 ) e. _V /\ ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) e. _V ) ) -> ( ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } ) )
186 74 184 75 80 185 mp4an 
 |-  ( ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
187 91 183 186 syl2anc 
 |-  ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
188 prcom 
 |-  { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } = { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) }
189 f1oeq3 
 |-  ( { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } = { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } -> ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } <-> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
190 188 189 ax-mp 
 |-  ( { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } <-> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
191 187 190 sylib 
 |-  ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
192 f1of1 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
193 36 192 syl 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
194 f1ores 
 |-  ( ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) /\ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> ( ( 2nd ` ( 1st ` U ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
195 193 24 194 syl2anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> ( ( 2nd ` ( 1st ` U ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
196 dff1o3 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` U ) ) ) )
197 196 simprbi 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` U ) ) )
198 imadif 
 |-  ( Fun `' ( 2nd ` ( 1st ` U ) ) -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
199 36 197 198 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
200 f1ofo 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
201 foima 
 |-  ( ( 2nd ` ( 1st ` U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
202 36 200 201 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
203 f1ofo 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
204 foima 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
205 59 203 204 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
206 202 205 eqtr4d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) )
207 128 rneqd 
 |-  ( ph -> ran ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ran ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
208 df-ima 
 |-  ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ran ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
209 df-ima 
 |-  ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ran ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
210 207 208 209 3eqtr4g 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
211 206 210 difeq12d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
212 dff1o3 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` T ) ) ) )
213 212 simprbi 
 |-  ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` T ) ) )
214 imadif 
 |-  ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
215 59 213 214 3syl 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
216 dfin4 
 |-  ( ( 1 ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
217 sseqin2 
 |-  ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) <-> ( ( 1 ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
218 24 217 sylib 
 |-  ( ph -> ( ( 1 ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
219 216 218 eqtr3id 
 |-  ( ph -> ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
220 219 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
221 215 220 eqtr3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
222 199 211 221 3eqtrd 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
223 219 imaeq2d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " ( ( 1 ... N ) \ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` U ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
224 fnimapr 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( 2nd ` T ) e. ( 1 ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
225 68 19 23 224 syl3anc 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) } )
226 225 188 eqtrdi 
 |-  ( ph -> ( ( 2nd ` ( 1st ` T ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
227 222 223 226 3eqtr3d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
228 227 f1oeq3d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> ( ( 2nd ` ( 1st ` U ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) <-> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
229 195 228 mpbid 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
230 ssabral 
 |-  ( { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } <-> A. f e. { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } )
231 f1oeq1 
 |-  ( f = ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) -> ( f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } <-> ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
232 f1oeq1 
 |-  ( f = { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } -> ( f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } <-> { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
233 f1oeq1 
 |-  ( f = ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } <-> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
234 144 145 146 231 232 233 raltp 
 |-  ( A. f e. { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } <-> ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } /\ ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
235 230 234 bitri 
 |-  ( { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } <-> ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } /\ { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } /\ ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) )
236 182 191 229 235 syl3anbrc 
 |-  ( ph -> { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } )
237 hashss 
 |-  ( ( { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } e. Fin /\ { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) <_ ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) )
238 163 236 237 sylancr 
 |-  ( ph -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) <_ ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) )
239 153 enref 
 |-  { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ~~ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) }
240 hashprg 
 |-  ( ( ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) e. _V /\ ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) e. _V ) -> ( ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) <-> ( # ` { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) = 2 ) )
241 80 184 240 mp2an 
 |-  ( ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) =/= ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) <-> ( # ` { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) = 2 )
242 96 241 sylib 
 |-  ( ph -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) = 2 )
243 hashprg 
 |-  ( ( ( 2nd ` T ) e. _V /\ ( ( 2nd ` T ) + 1 ) e. _V ) -> ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) <-> ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = 2 ) )
244 74 75 243 mp2an 
 |-  ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) <-> ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = 2 )
245 91 244 sylib 
 |-  ( ph -> ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = 2 )
246 242 245 eqtr4d 
 |-  ( ph -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) = ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
247 hashen 
 |-  ( ( { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } e. Fin /\ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. Fin ) -> ( ( # ` { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) = ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) <-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ~~ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
248 155 156 247 mp2an 
 |-  ( ( # ` { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ) = ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) <-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ~~ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
249 246 248 sylib 
 |-  ( ph -> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ~~ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
250 hashfacen 
 |-  ( ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ~~ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } /\ { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } ~~ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ~~ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } )
251 239 249 250 sylancr 
 |-  ( ph -> { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ~~ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } )
252 153 153 mapval 
 |-  ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ^m { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } }
253 mapfi 
 |-  ( ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. Fin /\ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. Fin ) -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ^m { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. Fin )
254 156 156 253 mp2an 
 |-  ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ^m { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. Fin
255 252 254 eqeltrri 
 |-  { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } e. Fin
256 f1of 
 |-  ( f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -> f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
257 256 ss2abi 
 |-  { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } }
258 ssfi 
 |-  ( ( { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } e. Fin /\ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } C_ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } --> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) -> { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } e. Fin )
259 255 257 258 mp2an 
 |-  { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } e. Fin
260 hashen 
 |-  ( ( { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } e. Fin /\ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } e. Fin ) -> ( ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) = ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) <-> { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ~~ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) )
261 163 259 260 mp2an 
 |-  ( ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) = ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) <-> { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ~~ { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } )
262 251 261 sylibr 
 |-  ( ph -> ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) = ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) )
263 hashfac 
 |-  ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } e. Fin -> ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) = ( ! ` ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
264 156 263 ax-mp 
 |-  ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) = ( ! ` ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
265 245 fveq2d 
 |-  ( ph -> ( ! ` ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ! ` 2 ) )
266 fac2 
 |-  ( ! ` 2 ) = 2
267 265 266 eqtrdi 
 |-  ( ph -> ( ! ` ( # ` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = 2 )
268 264 267 eqtrid 
 |-  ( ph -> ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } } ) = 2 )
269 262 268 eqtrd 
 |-  ( ph -> ( # ` { f | f : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) } } ) = 2 )
270 238 269 breqtrd 
 |-  ( ph -> ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) <_ 2 )
271 breq1 
 |-  ( ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 -> ( ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) <_ 2 <-> 3 <_ 2 ) )
272 270 271 syl5ibcom 
 |-  ( ph -> ( ( # ` { ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) , { <. ( 2nd ` T ) , ( ( 2nd ` ( 1st ` T ) ) ` ( 2nd ` T ) ) >. , <. ( ( 2nd ` T ) + 1 ) , ( ( 2nd ` ( 1st ` T ) ) ` ( ( 2nd ` T ) + 1 ) ) >. } , ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) } ) = 3 -> 3 <_ 2 ) )
273 151 272 syld 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) =/= ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) -> 3 <_ 2 ) )
274 273 necon1bd 
 |-  ( ph -> ( -. 3 <_ 2 -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) ) )
275 46 274 mpi 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) )
276 coires1 
 |-  ( ( 2nd ` ( 1st ` T ) ) o. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 2nd ` ( 1st ` T ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
277 128 276 eqtr4di 
 |-  ( ph -> ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
278 275 277 uneq12d 
 |-  ( ph -> ( ( ( 2nd ` ( 1st ` U ) ) |` { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( 2nd ` ( 1st ` U ) ) |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) u. ( ( 2nd ` ( 1st ` T ) ) o. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )
279 41 278 eqtr3d 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) u. ( ( 2nd ` ( 1st ` T ) ) o. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )
280 coundi 
 |-  ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } ) u. ( ( 2nd ` ( 1st ` T ) ) o. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) )
281 279 280 eqtr4di 
 |-  ( ph -> ( 2nd ` ( 1st ` U ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )