Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem9 Structured version   Unicode version

Theorem poimirlem9 31913
Description: Lemma for poimir 31937, 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.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) } ) ) ) ) )
Distinct variable groups:    f, j,
t, y    ph, j, y   
j, F, y    j, N, y    T, j, y    U, j, y    ph, t    f, K, j, t    f, N, t    T, f    U, f    f, F, t    t, T    t, U    S, j,
t, y
Allowed substitution hints:    ph( f)    S( f)    K( y)

Proof of Theorem poimirlem9
StepHypRef Expression
1 resundi 5137 . . . 4  |-  ( ( 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 ) } ) ) )
2 poimir.0 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
32nncnd 10632 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  CC )
4 npcan1 10051 . . . . . . . . . . . 12  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
53, 4syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
62nnzd 11046 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
7 peano2zm 10987 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
8 uzid 11180 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
9 peano2uz 11219 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
106, 7, 8, 94syl 19 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
115, 10eqeltrrd 2508 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
12 fzss2 11845 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 1 ... ( N  - 
1 ) )  C_  ( 1 ... N
) )
1311, 12syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 1 ... N ) )
14 poimirlem9.2 . . . . . . . . 9  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) )
1513, 14sseldd 3465 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... N ) )
16 fzp1elp1 11856 . . . . . . . . . 10  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  (
( 2nd `  T
)  +  1 )  e.  ( 1 ... ( ( N  - 
1 )  +  1 ) ) )
1714, 16syl 17 . . . . . . . . 9  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... ( ( N  - 
1 )  +  1 ) ) )
185oveq2d 6321 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
1917, 18eleqtrd 2509 . . . . . . . 8  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )
20 prssi 4156 . . . . . . . 8  |-  ( ( ( 2nd `  T
)  e.  ( 1 ... N )  /\  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
2115, 19, 20syl2anc 665 . . . . . . 7  |-  ( ph  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
22 undif 3878 . . . . . . 7  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N )  <->  ( {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( 1 ... N ) )
2321, 22sylib 199 . . . . . 6  |-  ( ph  ->  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  =  ( 1 ... N
) )
2423reseq2d 5124 . . . . 5  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( ( 2nd `  ( 1st `  U
) )  |`  (
1 ... N ) ) )
25 poimirlem9.3 . . . . . . . 8  |-  ( ph  ->  U  e.  S )
26 elrabi 3225 . . . . . . . . 9  |-  ( 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 ) ) )
27 poimirlem22.s . . . . . . . . 9  |-  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 } ) ) ) ) }
2826, 27eleq2s 2527 . . . . . . . 8  |-  ( U  e.  S  ->  U  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
29 xp1st 6837 . . . . . . . 8  |-  ( 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 ) } ) )
30 xp2nd 6838 . . . . . . . 8  |-  ( ( 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 ) } )
3125, 28, 29, 304syl 19 . . . . . . 7  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
32 fvex 5891 . . . . . . . 8  |-  ( 2nd `  ( 1st `  U
) )  e.  _V
33 f1oeq1 5822 . . . . . . . 8  |-  ( f  =  ( 2nd `  ( 1st `  U ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
3432, 33elab 3217 . . . . . . 7  |-  ( ( 2nd `  ( 1st `  U ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
3531, 34sylib 199 . . . . . 6  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
36 f1ofn 5832 . . . . . 6  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  U
) )  Fn  (
1 ... N ) )
37 fnresdm 5703 . . . . . 6  |-  ( ( 2nd `  ( 1st `  U ) )  Fn  ( 1 ... N
)  ->  ( ( 2nd `  ( 1st `  U
) )  |`  (
1 ... N ) )  =  ( 2nd `  ( 1st `  U ) ) )
3835, 36, 373syl 18 . . . . 5  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  ( 1 ... N
) )  =  ( 2nd `  ( 1st `  U ) ) )
3924, 38eqtrd 2463 . . . 4  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( 2nd `  ( 1st `  U ) ) )
401, 39syl5eqr 2477 . . 3  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) )  |`  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) } )  u.  ( ( 2nd `  ( 1st `  U ) )  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )  =  ( 2nd `  ( 1st `  U ) ) )
41 2lt3 10784 . . . . . 6  |-  2  <  3
42 2re 10686 . . . . . . 7  |-  2  e.  RR
43 3re 10690 . . . . . . 7  |-  3  e.  RR
4442, 43ltnlei 9762 . . . . . 6  |-  ( 2  <  3  <->  -.  3  <_  2 )
4541, 44mpbi 211 . . . . 5  |-  -.  3  <_  2
46 df-pr 4001 . . . . . . . . . . . 12  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  =  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. }  u.  { <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } )
4746coeq2i 5014 . . . . . . . . . . 11  |-  ( ( 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
) >. } ) )
48 coundi 5355 . . . . . . . . . . 11  |-  ( ( 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
) >. } ) )
4947, 48eqtri 2451 . . . . . . . . . 10  |-  ( ( 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
) >. } ) )
50 poimirlem9.1 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  S )
51 elrabi 3225 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
5251, 27eleq2s 2527 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 6837 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 6838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) } )
5550, 52, 53, 544syl 19 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
56 fvex 5891 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
57 f1oeq1 5822 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
5856, 57elab 3217 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
5955, 58sylib 199 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
60 f1of1 5830 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-1-1-> ( 1 ... N
) )
6159, 60syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-> ( 1 ... N ) )
6219snssd 4145 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { ( ( 2nd `  T )  +  1 ) }  C_  (
1 ... N ) )
63 f1ores 5845 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) } ) )
6461, 62, 63syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) : { ( ( 2nd `  T )  +  1 ) } -1-1-onto-> ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) } ) )
65 f1of 5831 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) } ) )
6664, 65syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) : { ( ( 2nd `  T )  +  1 ) } --> ( ( 2nd `  ( 1st `  T ) ) " { ( ( 2nd `  T )  +  1 ) } ) )
67 f1ofn 5832 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
6859, 67syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
69 fnsnfv 5941 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N )  /\  (
( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )  ->  { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) }  =  ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) } ) )
7068, 19, 69syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) }  =  ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) } ) )
7170feq3d 5734 . . . . . . . . . . . . . . 15  |-  ( 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 ) } ) ) )
7266, 71mpbird 235 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) : { ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } )
73 eqid 2422 . . . . . . . . . . . . . . 15  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. }  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. }
74 fvex 5891 . . . . . . . . . . . . . . . 16  |-  ( 2nd `  T )  e.  _V
75 ovex 6333 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  T )  +  1 )  e. 
_V
7674, 75fsn 6076 . . . . . . . . . . . . . . 15  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. } : { ( 2nd `  T ) } --> { ( ( 2nd `  T
)  +  1 ) }  <->  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. }  =  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } )
7773, 76mpbir 212 . . . . . . . . . . . . . 14  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. } : {
( 2nd `  T
) } --> { ( ( 2nd `  T
)  +  1 ) }
78 fco2 5757 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) } )
7972, 77, 78sylancl 666 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } ) : {
( 2nd `  T
) } --> { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } )
80 fvex 5891 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) )  e.  _V
8180fconst2 6136 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) } ) )
8279, 81sylib 199 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } )  =  ( { ( 2nd `  T
) }  X.  {
( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } ) )
8374, 80xpsn 6081 . . . . . . . . . . . 12  |-  ( { ( 2nd `  T
) }  X.  {
( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } )  =  { <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >. }
8482, 83syl6eq 2479 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } )  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >. } )
8584uneq1d 3619 . . . . . . . . . 10  |-  ( 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
) >. } ) ) )
8649, 85syl5eq 2475 . . . . . . . . 9  |-  ( 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 11835 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  NN )
8814, 87syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2nd `  T
)  e.  NN )
8988nnred 10631 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  T
)  e.  RR )
9089ltp1d 10544 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  T
)  <  ( ( 2nd `  T )  +  1 ) )
9189, 90ltned 9778 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2nd `  T
)  =/=  ( ( 2nd `  T )  +  1 ) )
9291necomd 2691 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  =/=  ( 2nd `  T
) )
93 f1veqaeq 6176 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
9461, 19, 15, 93syl12anc 1262 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) )  =  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) )  ->  ( ( 2nd `  T )  +  1 )  =  ( 2nd `  T ) ) )
9594necon3d 2644 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  T )  +  1 )  =/=  ( 2nd `  T )  ->  (
( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) )  =/=  (
( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) ) )
9692, 95mpd 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) )  =/=  (
( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) )
9796neneqd 2621 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) )  =  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) )
9874, 80opth 4695 . . . . . . . . . . . 12  |-  ( <.
( 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
) ) ) )
9998simprbi 465 . . . . . . . . . . 11  |-  ( <.
( 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 ) ) )
10097, 99nsyl 124 . . . . . . . . . 10  |-  ( ph  ->  -.  <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >.  =  <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T
) ) `  ( 2nd `  T ) )
>. )
10191neneqd 2621 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( 2nd `  T
)  =  ( ( 2nd `  T )  +  1 ) )
10274, 80opth1 4694 . . . . . . . . . . 11  |-  ( <.
( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >.  =  <. ( ( 2nd `  T
)  +  1 ) ,  ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) >.  ->  ( 2nd `  T )  =  ( ( 2nd `  T
)  +  1 ) )
103101, 102nsyl 124 . . . . . . . . . 10  |-  ( ph  ->  -.  <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >.  =  <. ( ( 2nd `  T
)  +  1 ) ,  ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) >. )
104 opex 4685 . . . . . . . . . . . . . . 15  |-  <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >.  e.  _V
105104snid 4026 . . . . . . . . . . . . . 14  |-  <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >.  e.  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >. }
106 elun1 3633 . . . . . . . . . . . . . 14  |-  ( <.
( 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
) >. } ) ) )
107105, 106ax-mp 5 . . . . . . . . . . . . 13  |-  <. ( 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 2496 . . . . . . . . . . . . 13  |-  ( ( { <. ( 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 ) ) >. } ) )
109107, 108mpbii 214 . . . . . . . . . . . 12  |-  ( ( { <. ( 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 ) ) >. } )
110104elpr 4016 . . . . . . . . . . . . 13  |-  ( <.
( 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 498 . . . . . . . . . . . . 13  |-  ( (
<. ( 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 ) ) >. ) )
112110, 111bitri 252 . . . . . . . . . . . 12  |-  ( <.
( 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 ) ) >. ) )
113109, 112sylib 199 . . . . . . . . . . 11  |-  ( ( { <. ( 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 ) ) >. ) )
114113necon2ai 2655 . . . . . . . . . 10  |-  ( ( -.  <. ( 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 ) ) >. } )
115100, 103, 114syl2anc 665 . . . . . . . . 9  |-  ( 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 ) ) >. } )
11686, 115eqnetrd 2713 . . . . . . . 8  |-  ( 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 6091 . . . . . . . . . . . 12  |-  ( ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N )  /\  ( 2nd `  T )  e.  ( 1 ... N
) )  ->  (
( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) } )  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) >. } )
11868, 15, 117syl2anc 665 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) } )  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) >. } )
119 fnressn 6091 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) >. } )
12068, 19, 119syl2anc 665 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } )  =  { <. ( ( 2nd `  T )  +  1 ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >. } )
121118, 120uneq12d 3621 . . . . . . . . . 10  |-  ( 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 4001 . . . . . . . . . . . 12  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  =  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } )
123122reseq2i 5121 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } ) )
124 resundi 5137 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } ) )  =  ( ( ( 2nd `  ( 1st `  T
) )  |`  { ( 2nd `  T ) } )  u.  (
( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) )
125123, 124eqtri 2451 . . . . . . . . . 10  |-  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ( ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) } )  u.  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) )
126 df-pr 4001 . . . . . . . . . 10  |-  { <. ( 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 ) ) >. } )
127121, 125, 1263eqtr4g 2488 . . . . . . . . 9  |-  ( 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 poimirlem9.4 . . . . . . . . . . 11  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) )  =/=  ( 2nd `  ( 1st `  T ) ) )
1292, 27, 50, 14, 25poimirlem8 31912 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( ( 2nd `  ( 1st `  T ) )  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
130 uneq12 3615 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) } ) ) ) )
131 resundi 5137 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) } ) ) )
13223reseq2d 5124 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( ( 2nd `  ( 1st `  T
) )  |`  (
1 ... N ) ) )
133 fnresdm 5703 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N
)  ->  ( ( 2nd `  ( 1st `  T
) )  |`  (
1 ... N ) )  =  ( 2nd `  ( 1st `  T ) ) )
13459, 67, 1333syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  ( 1 ... N
) )  =  ( 2nd `  ( 1st `  T ) ) )
135132, 134eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( 2nd `  ( 1st `  T ) ) )
136131, 135syl5eqr 2477 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) )  |`  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) } )  u.  ( ( 2nd `  ( 1st `  T ) )  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )  =  ( 2nd `  ( 1st `  T ) ) )
13740, 136eqeq12d 2444 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
138130, 137syl5ib 222 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )
139129, 138mpan2d 678 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) )  |`  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) } )  =  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  ->  ( 2nd `  ( 1st `  U
) )  =  ( 2nd `  ( 1st `  T ) ) ) )
140139necon3d 2644 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  =/=  ( 2nd `  ( 1st `  T ) )  ->  ( ( 2nd `  ( 1st `  U
) )  |`  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) } )  =/=  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
141128, 140mpd 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =/=  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
142141necomd 2691 . . . . . . . . 9  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =/=  ( ( 2nd `  ( 1st `  U ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
143127, 142eqnetrrd 2714 . . . . . . . 8  |-  ( 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 ) } ) )
144 prex 4663 . . . . . . . . . . . 12  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  e.  _V
14556, 144coex 6759 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  T ) )  o. 
{ <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )  e.  _V
146 prex 4663 . . . . . . . . . . 11  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T
) ) `  ( 2nd `  T ) )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >. }  e.  _V
14732resex 5167 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  U ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  e.  _V
148 hashtpg 12645 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
149145, 146, 147, 148mp3an 1360 . . . . . . . . . 10  |-  ( ( ( ( 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 )
150149biimpi 197 . . . . . . . . 9  |-  ( ( ( ( 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 )
1511503expia 1207 . . . . . . . 8  |-  ( ( ( ( 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 ) )
152116, 143, 151syl2anc 665 . . . . . . 7  |-  ( 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 ) )
153 prex 4663 . . . . . . . . . . . . 13  |-  { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) }  e.  _V
154 prex 4663 . . . . . . . . . . . . 13  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  e.  _V
155153, 154mapval 7495 . . . . . . . . . . . 12  |-  ( { ( ( 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 ) ) } }
156 prfi 7855 . . . . . . . . . . . . 13  |-  { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) }  e.  Fin
157 prfi 7855 . . . . . . . . . . . . 13  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  e.  Fin
158 mapfi 7879 . . . . . . . . . . . . 13  |-  ( ( { ( ( 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 )
159156, 157, 158mp2an 676 . . . . . . . . . . . 12  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) }  ^m  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  e.  Fin
160155, 159eqeltrri 2504 . . . . . . . . . . 11  |-  { f  |  f : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) } }  e.  Fin
161 f1of 5831 . . . . . . . . . . . 12  |-  ( 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 ) ) } )
162161ss2abi 3533 . . . . . . . . . . 11  |-  { 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 ) ) } }
163 ssfi 7801 . . . . . . . . . . 11  |-  ( ( { 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 )
164160, 162, 163mp2an 676 . . . . . . . . . 10  |-  { f  |  f : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) } }  e.  Fin
165 prssi 4156 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N )  /\  ( 2nd `  T )  e.  ( 1 ... N
) )  ->  { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  C_  (
1 ... N ) )
16619, 15, 165syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  C_  ( 1 ... N
) )
167 f1ores 5845 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) } ) )
16861, 166, 167syl2anc 665 . . . . . . . . . . . . . 14  |-  ( 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
) } ) )
169 fnimapr 5945 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) } )
17068, 19, 15, 169syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) } )  =  { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) } )
171 f1oeq3 5824 . . . . . . . . . . . . . . 15  |-  ( ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) } )  =  { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 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 `  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 ) ) } ) )
172170, 171syl 17 . . . . . . . . . . . . . 14  |-  ( 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 ) ) } ) )
173168, 172mpbid 213 . . . . . . . . . . . . 13  |-  ( 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 ) ) } )
174 f1oprg 5871 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
) } ) )
17574, 75, 75, 74, 174mp4an 677 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) } )
17691, 92, 175syl2anc 665 . . . . . . . . . . . . 13  |-  ( ph  ->  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) } )
177 f1oco 5853 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) } )
178173, 176, 177syl2anc 665 . . . . . . . . . . . 12  |-  ( 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 ) ) } )
179 rnpropg 5335 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) } )
18074, 75, 179mp2an 676 . . . . . . . . . . . . . 14  |-  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  =  { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }
181180eqimssi 3518 . . . . . . . . . . . . 13  |-  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  C_  { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }
182 cores 5357 . . . . . . . . . . . . 13  |-  ( 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
) >. } ) )
183 f1oeq1 5822 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) } ) )
184181, 182, 183mp2b 10 . . . . . . . . . . . 12  |-  ( ( ( ( 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