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

Theorem poimirlem9 32013
Description: Lemma for poimir 32037, 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 5124 . . . 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 10647 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  CC )
4 npcan1 10065 . . . . . . . . . . . 12  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
53, 4syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
62nnzd 11062 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
7 peano2zm 11004 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
8 uzid 11197 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
9 peano2uz 11235 . . . . . . . . . . . 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 2550 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
12 fzss2 11864 . . . . . . . . . 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 3419 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... N ) )
16 fzp1elp1 11875 . . . . . . . . . 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 6324 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
1917, 18eleqtrd 2551 . . . . . . . 8  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )
20 prssi 4119 . . . . . . . 8  |-  ( ( ( 2nd `  T
)  e.  ( 1 ... N )  /\  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
2115, 19, 20syl2anc 673 . . . . . . 7  |-  ( ph  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
22 undif 3839 . . . . . . 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 201 . . . . . 6  |-  ( ph  ->  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  =  ( 1 ... N
) )
2423reseq2d 5111 . . . . 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 3181 . . . . . . . . 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 2567 . . . . . . . 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 6842 . . . . . . . 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 6843 . . . . . . . 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 5889 . . . . . . . 8  |-  ( 2nd `  ( 1st `  U
) )  e.  _V
33 f1oeq1 5818 . . . . . . . 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 3173 . . . . . . 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 201 . . . . . 6  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
36 f1ofn 5829 . . . . . 6  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  U
) )  Fn  (
1 ... N ) )
37 fnresdm 5695 . . . . . 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 2505 . . . 4  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( 2nd `  ( 1st `  U ) ) )
401, 39syl5eqr 2519 . . 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 10800 . . . . . 6  |-  2  <  3
42 2re 10701 . . . . . . 7  |-  2  e.  RR
43 3re 10705 . . . . . . 7  |-  3  e.  RR
4442, 43ltnlei 9773 . . . . . 6  |-  ( 2  <  3  <->  -.  3  <_  2 )
4541, 44mpbi 213 . . . . 5  |-  -.  3  <_  2
46 df-pr 3962 . . . . . . . . . . . 12  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  =  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. }  u.  { <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } )
4746coeq2i 5000 . . . . . . . . . . 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 5343 . . . . . . . . . . 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 2493 . . . . . . . . . 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 3181 . . . . . . . . . . . . . . . . . . . . 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 2567 . . . . . . . . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . . . . . . . . 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 6843 . . . . . . . . . . . . . . . . . . . 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 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
57 f1oeq1 5818 . . . . . . . . . . . . . . . . . . . 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 3173 . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
60 f1of1 5827 . . . . . . . . . . . . . . . . . 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 4108 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { ( ( 2nd `  T )  +  1 ) }  C_  (
1 ... N ) )
63 f1ores 5842 . . . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) : { ( ( 2nd `  T )  +  1 ) } -1-1-onto-> ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) } ) )
65 f1of 5828 . . . . . . . . . . . . . . . 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 5829 . . . . . . . . . . . . . . . . . 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 5940 . . . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) }  =  ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) } ) )
7170feq3d 5726 . . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) : { ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } )
73 eqid 2471 . . . . . . . . . . . . . . 15  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. }  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. }
74 fvex 5889 . . . . . . . . . . . . . . . 16  |-  ( 2nd `  T )  e.  _V
75 ovex 6336 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  T )  +  1 )  e. 
_V
7674, 75fsn 6077 . . . . . . . . . . . . . . 15  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. } : { ( 2nd `  T ) } --> { ( ( 2nd `  T
)  +  1 ) }  <->  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. }  =  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } )
7773, 76mpbir 214 . . . . . . . . . . . . . 14  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. } : {
( 2nd `  T
) } --> { ( ( 2nd `  T
)  +  1 ) }
78 fco2 5752 . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } ) : {
( 2nd `  T
) } --> { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } )
80 fvex 5889 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) )  e.  _V
8180fconst2 6137 . . . . . . . . . . . . 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 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } )  =  ( { ( 2nd `  T
) }  X.  {
( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } ) )
8374, 80xpsn 6082 . . . . . . . . . . . 12  |-  ( { ( 2nd `  T
) }  X.  {
( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) } )  =  { <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >. }
8482, 83syl6eq 2521 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. } )  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >. } )
8584uneq1d 3578 . . . . . . . . . 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 2517 . . . . . . . . 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 11854 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  NN )
8814, 87syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2nd `  T
)  e.  NN )
8988nnred 10646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  T
)  e.  RR )
9089ltp1d 10559 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  T
)  <  ( ( 2nd `  T )  +  1 ) )
9189, 90ltned 9788 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2nd `  T
)  =/=  ( ( 2nd `  T )  +  1 ) )
9291necomd 2698 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  =/=  ( 2nd `  T
) )
93 f1veqaeq 6179 . . . . . . . . . . . . . . 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 1290 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) )  =  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) )  ->  ( ( 2nd `  T )  +  1 )  =  ( 2nd `  T ) ) )
9594necon3d 2664 . . . . . . . . . . . . 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 2648 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) )  =  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) )
9874, 80opth 4676 . . . . . . . . . . . 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 471 . . . . . . . . . . 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 125 . . . . . . . . . 10  |-  ( ph  ->  -.  <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >.  =  <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T
) ) `  ( 2nd `  T ) )
>. )
10191neneqd 2648 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( 2nd `  T
)  =  ( ( 2nd `  T )  +  1 ) )
10274, 80opth1 4675 . . . . . . . . . . 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 125 . . . . . . . . . 10  |-  ( ph  ->  -.  <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >.  =  <. ( ( 2nd `  T
)  +  1 ) ,  ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) >. )
104 opex 4664 . . . . . . . . . . . . . . 15  |-  <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >.  e.  _V
105104snid 3988 . . . . . . . . . . . . . 14  |-  <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >.  e.  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >. }
106 elun1 3592 . . . . . . . . . . . . . 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 2538 . . . . . . . . . . . . 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 216 . . . . . . . . . . . 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 3977 . . . . . . . . . . . . 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 504 . . . . . . . . . . . . 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 257 . . . . . . . . . . . 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 201 . . . . . . . . . . 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 2672 . . . . . . . . . 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 673 . . . . . . . . 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 2710 . . . . . . . 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 6092 . . . . . . . . . . . 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 673 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) } )  =  { <. ( 2nd `  T
) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) >. } )
119 fnressn 6092 . . . . . . . . . . . 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 673 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } )  =  { <. ( ( 2nd `  T )  +  1 ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( ( 2nd `  T
)  +  1 ) ) >. } )
121118, 120uneq12d 3580 . . . . . . . . . 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 3962 . . . . . . . . . . . 12  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  =  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } )
123122reseq2i 5108 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } ) )
124 resundi 5124 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } ) )  =  ( ( ( 2nd `  ( 1st `  T
) )  |`  { ( 2nd `  T ) } )  u.  (
( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) )
125123, 124eqtri 2493 . . . . . . . . . 10  |-  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ( ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) } )  u.  ( ( 2nd `  ( 1st `  T ) )  |`  { ( ( 2nd `  T )  +  1 ) } ) )
126 df-pr 3962 . . . . . . . . . 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 2530 . . . . . . . . 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 32012 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( ( 2nd `  ( 1st `  T ) )  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
130 uneq12 3574 . . . . . . . . . . . . . 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 5124 . . . . . . . . . . . . . . . 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 5111 . . . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . . . . . 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 2505 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( 2nd `  ( 1st `  T ) ) )
136131, 135syl5eqr 2519 . . . . . . . . . . . . . . 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 2486 . . . . . . . . . . . . . 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 227 . . . . . . . . . . . . 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 688 . . . . . . . . . . . 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 2664 . . . . . . . . . . 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 2698 . . . . . . . . 9  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =/=  ( ( 2nd `  ( 1st `  U ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
143127, 142eqnetrrd 2711 . . . . . . . 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 4642 . . . . . . . . . . . 12  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  e.  _V
14556, 144coex 6764 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  T ) )  o. 
{ <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )  e.  _V
146 prex 4642 . . . . . . . . . . 11  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  ( 1st `  T
) ) `  ( 2nd `  T ) )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) >. }  e.  _V
14732resex 5154 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  U ) )  |`  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  e.  _V
148 hashtpg 12682 . . . . . . . . . . 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 1390 . . . . . . . . . 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 199 . . . . . . . . 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 1233 . . . . . . . 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 673 . . . . . . 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 4642 . . . . . . . . . . . . 13  |-  { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) }  e.  _V
154 prex 4642 . . . . . . . . . . . . 13  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  e.  _V
155153, 154mapval 7502 . . . . . . . . . . . 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 7864 . . . . . . . . . . . . 13  |-  { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) }  e.  Fin
157 prfi 7864 . . . . . . . . . . . . 13  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  e.  Fin
158 mapfi 7888 . . . . . . . . . . . . 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 686 . . . . . . . . . . . 12  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 ( ( 2nd `  T )  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `
 ( 2nd `  T
) ) }  ^m  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  e.  Fin
160155, 159eqeltrri 2546 . . . . . . . . . . 11  |-  { f  |  f : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) } }  e.  Fin
161 f1of 5828 . . . . . . . . . . . 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 3487 . . . . . . . . . . 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 7810 . . . . . . . . . . 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 686 . . . . . . . . . 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 4119 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N )  /\  ( 2nd `  T )  e.  ( 1 ... N
) )  ->  { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  C_  (
1 ... N ) )
16619, 15, 165syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( ph  ->  { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  C_  ( 1 ... N
) )
167 f1ores 5842 . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . 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 5944 . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) } )  =  { ( ( 2nd `  ( 1st `  T
) ) `  (
( 2nd `  T
)  +  1 ) ) ,  ( ( 2nd `  ( 1st `  T ) ) `  ( 2nd `  T ) ) } )
171 f1oeq3 5820 . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . 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 5869 . . . . . . . . . . . . . . 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 687 . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . 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 5850 . . . . . . . . . . . . 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 673 . . . . . . . . . . . 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 5323 . . . . . . . . . . . . . . 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 686 . . . . . . . . . . . . . 14  |-  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  =  { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }
181180eqimssi 3472 . . . . . . . . . . . . 13  |-  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  C_  { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }
182 cores 5345 . . . . . . . . . . . . 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 5818 . . . . . . . . . . . . 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
) ) }  <->  (