MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  swrdccat3 Structured version   Unicode version

Theorem swrdccat3 12676
Description: The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 28-May-2018.)
Hypothesis
Ref Expression
swrdccatin12.l  |-  L  =  ( # `  A
)
Assertion
Ref Expression
swrdccat3  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  if ( N  <_  L ,  ( A substr  <. M ,  N >. ) ,  if ( L  <_  M , 
( B substr  <. ( M  -  L ) ,  ( N  -  L
) >. ) ,  ( ( A substr  <. M ,  L >. ) concat  ( B substr  <.
0 ,  ( N  -  L ) >.
) ) ) ) ) )

Proof of Theorem swrdccat3
StepHypRef Expression
1 simpll 753 . . . 4  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  N  <_  L )  ->  ( A  e. Word  V  /\  B  e. Word  V ) )
2 simpl 457 . . . . . 6  |-  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  ->  M  e.  ( 0 ... N ) )
32ad2antlr 726 . . . . 5  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  N  <_  L )  ->  M  e.  ( 0 ... N
) )
4 lencl 12524 . . . . . . . . 9  |-  ( A  e. Word  V  ->  ( # `
 A )  e. 
NN0 )
5 elfznn0 11766 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( 0 ... ( L  +  (
# `  B )
) )  ->  N  e.  NN0 )
65adantr 465 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( 0 ... ( L  +  ( # `  B ) ) )  /\  ( # `
 A )  e. 
NN0 )  ->  N  e.  NN0 )
76adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  ( 0 ... ( L  +  ( # `  B
) ) )  /\  ( # `  A )  e.  NN0 )  /\  N  <_  L )  ->  N  e.  NN0 )
8 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  ( 0 ... ( L  +  ( # `  B
) ) )  /\  ( # `  A )  e.  NN0 )  /\  N  <_  L )  -> 
( # `  A )  e.  NN0 )
9 swrdccatin12.l . . . . . . . . . . . . . . . 16  |-  L  =  ( # `  A
)
109breq2i 4455 . . . . . . . . . . . . . . 15  |-  ( N  <_  L  <->  N  <_  (
# `  A )
)
1110biimpi 194 . . . . . . . . . . . . . 14  |-  ( N  <_  L  ->  N  <_  ( # `  A
) )
1211adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  ( 0 ... ( L  +  ( # `  B
) ) )  /\  ( # `  A )  e.  NN0 )  /\  N  <_  L )  ->  N  <_  ( # `  A
) )
13 elfz2nn0 11764 . . . . . . . . . . . . 13  |-  ( N  e.  ( 0 ... ( # `  A
) )  <->  ( N  e.  NN0  /\  ( # `  A )  e.  NN0  /\  N  <_  ( # `  A
) ) )
147, 8, 12, 13syl3anbrc 1180 . . . . . . . . . . . 12  |-  ( ( ( N  e.  ( 0 ... ( L  +  ( # `  B
) ) )  /\  ( # `  A )  e.  NN0 )  /\  N  <_  L )  ->  N  e.  ( 0 ... ( # `  A
) ) )
1514ex 434 . . . . . . . . . . 11  |-  ( ( N  e.  ( 0 ... ( L  +  ( # `  B ) ) )  /\  ( # `
 A )  e. 
NN0 )  ->  ( N  <_  L  ->  N  e.  ( 0 ... ( # `
 A ) ) ) )
1615ex 434 . . . . . . . . . 10  |-  ( N  e.  ( 0 ... ( L  +  (
# `  B )
) )  ->  (
( # `  A )  e.  NN0  ->  ( N  <_  L  ->  N  e.  ( 0 ... ( # `
 A ) ) ) ) )
1716adantl 466 . . . . . . . . 9  |-  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( ( # `  A
)  e.  NN0  ->  ( N  <_  L  ->  N  e.  ( 0 ... ( # `  A
) ) ) ) )
184, 17syl5com 30 . . . . . . . 8  |-  ( A  e. Word  V  ->  (
( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( N  <_  L  ->  N  e.  ( 0 ... ( # `  A ) ) ) ) )
1918adantr 465 . . . . . . 7  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( N  <_  L  ->  N  e.  ( 0 ... ( # `  A ) ) ) ) )
2019imp 429 . . . . . 6  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( N  <_  L  ->  N  e.  ( 0 ... ( # `
 A ) ) ) )
2120imp 429 . . . . 5  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  N  <_  L )  ->  N  e.  ( 0 ... ( # `
 A ) ) )
223, 21jca 532 . . . 4  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  N  <_  L )  ->  ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( # `  A
) ) ) )
23 swrdccatin1 12667 . . . 4  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( # `
 A ) ) )  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  ( A substr  <. M ,  N >. ) ) )
241, 22, 23sylc 60 . . 3  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  N  <_  L )  ->  (
( A concat  B ) substr  <. M ,  N >. )  =  ( A substr  <. M ,  N >. ) )
25 simp1l 1020 . . . 4  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  L  <_  M )  ->  ( A  e. Word  V  /\  B  e. Word  V ) )
269eleq1i 2544 . . . . . . . . . . 11  |-  ( L  e.  NN0  <->  ( # `  A
)  e.  NN0 )
27 elfz2nn0 11764 . . . . . . . . . . . . . 14  |-  ( M  e.  ( 0 ... N )  <->  ( M  e.  NN0  /\  N  e. 
NN0  /\  M  <_  N ) )
28 nn0z 10883 . . . . . . . . . . . . . . . . . . . 20  |-  ( L  e.  NN0  ->  L  e.  ZZ )
2928adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  /\  L  e.  NN0 )  ->  L  e.  ZZ )
30 nn0z 10883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  N  e.  ZZ )
31303ad2ant2 1018 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  ->  N  e.  ZZ )
3231adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  /\  L  e.  NN0 )  ->  N  e.  ZZ )
33 nn0z 10883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  NN0  ->  M  e.  ZZ )
34333ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  ->  M  e.  ZZ )
3534adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  /\  L  e.  NN0 )  ->  M  e.  ZZ )
3629, 32, 353jca 1176 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  /\  L  e.  NN0 )  -> 
( L  e.  ZZ  /\  N  e.  ZZ  /\  M  e.  ZZ )
)
3736adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( M  e. 
NN0  /\  N  e.  NN0 
/\  M  <_  N
)  /\  L  e.  NN0 )  /\  L  <_  M )  ->  ( L  e.  ZZ  /\  N  e.  ZZ  /\  M  e.  ZZ ) )
38 simpl3 1001 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  /\  L  e.  NN0 )  ->  M  <_  N )
3938anim1i 568 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( M  e. 
NN0  /\  N  e.  NN0 
/\  M  <_  N
)  /\  L  e.  NN0 )  /\  L  <_  M )  ->  ( M  <_  N  /\  L  <_  M ) )
4039ancomd 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( M  e. 
NN0  /\  N  e.  NN0 
/\  M  <_  N
)  /\  L  e.  NN0 )  /\  L  <_  M )  ->  ( L  <_  M  /\  M  <_  N ) )
41 elfz2 11675 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ( L ... N )  <->  ( ( L  e.  ZZ  /\  N  e.  ZZ  /\  M  e.  ZZ )  /\  ( L  <_  M  /\  M  <_  N ) ) )
4237, 40, 41sylanbrc 664 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( M  e. 
NN0  /\  N  e.  NN0 
/\  M  <_  N
)  /\  L  e.  NN0 )  /\  L  <_  M )  ->  M  e.  ( L ... N
) )
4342ex 434 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  /\  L  e.  NN0 )  -> 
( L  <_  M  ->  M  e.  ( L ... N ) ) )
4443ex 434 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  ->  ( L  e.  NN0  ->  ( L  <_  M  ->  M  e.  ( L ... N
) ) ) )
4527, 44sylbi 195 . . . . . . . . . . . . 13  |-  ( M  e.  ( 0 ... N )  ->  ( L  e.  NN0  ->  ( L  <_  M  ->  M  e.  ( L ... N
) ) ) )
4645adantr 465 . . . . . . . . . . . 12  |-  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( L  e.  NN0  ->  ( L  <_  M  ->  M  e.  ( L ... N ) ) ) )
4746com12 31 . . . . . . . . . . 11  |-  ( L  e.  NN0  ->  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( L  <_  M  ->  M  e.  ( L ... N ) ) ) )
4826, 47sylbir 213 . . . . . . . . . 10  |-  ( (
# `  A )  e.  NN0  ->  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( L  <_  M  ->  M  e.  ( L ... N ) ) ) )
494, 48syl 16 . . . . . . . . 9  |-  ( A  e. Word  V  ->  (
( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( L  <_  M  ->  M  e.  ( L ... N ) ) ) )
5049adantr 465 . . . . . . . 8  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( L  <_  M  ->  M  e.  ( L ... N ) ) ) )
5150imp 429 . . . . . . 7  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( L  <_  M  ->  M  e.  ( L ... N ) ) )
5251a1d 25 . . . . . 6  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  N  <_  L  ->  ( L  <_  M  ->  M  e.  ( L ... N
) ) ) )
53523imp 1190 . . . . 5  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  L  <_  M )  ->  M  e.  ( L ... N
) )
54 elfz2nn0 11764 . . . . . . . . . . . 12  |-  ( N  e.  ( 0 ... ( L  +  (
# `  B )
) )  <->  ( N  e.  NN0  /\  ( L  +  ( # `  B
) )  e.  NN0  /\  N  <_  ( L  +  ( # `  B
) ) ) )
55 nn0z 10883 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  A )  e.  NN0  ->  ( # `  A
)  e.  ZZ )
569, 55syl5eqel 2559 . . . . . . . . . . . . . . . . 17  |-  ( (
# `  A )  e.  NN0  ->  L  e.  ZZ )
5756adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( # `  A
)  e.  NN0  /\  -.  N  <_  L )  ->  L  e.  ZZ )
5857adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  ->  L  e.  ZZ )
59 nn0z 10883 . . . . . . . . . . . . . . . . 17  |-  ( ( L  +  ( # `  B ) )  e. 
NN0  ->  ( L  +  ( # `  B ) )  e.  ZZ )
60593ad2ant2 1018 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  ( L  +  ( # `  B
) )  e.  ZZ )
6160adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  -> 
( L  +  (
# `  B )
)  e.  ZZ )
62303ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  N  e.  ZZ )
6362adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  ->  N  e.  ZZ )
6458, 61, 633jca 1176 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  -> 
( L  e.  ZZ  /\  ( L  +  (
# `  B )
)  e.  ZZ  /\  N  e.  ZZ )
)
659eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( # `  A )  =  L
6665eleq1i 2544 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  A )  e.  NN0  <->  L  e.  NN0 )
67 nn0re 10800 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( L  e.  NN0  ->  L  e.  RR )
68 nn0re 10800 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  N  e.  RR )
69 ltnle 9660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( L  e.  RR  /\  N  e.  RR )  ->  ( L  <  N  <->  -.  N  <_  L )
)
7067, 68, 69syl2anr 478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  NN0  /\  L  e.  NN0 )  -> 
( L  <  N  <->  -.  N  <_  L )
)
7170bicomd 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  L  e.  NN0 )  -> 
( -.  N  <_  L 
<->  L  <  N ) )
72 ltle 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( L  e.  RR  /\  N  e.  RR )  ->  ( L  <  N  ->  L  <_  N )
)
7367, 68, 72syl2anr 478 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  L  e.  NN0 )  -> 
( L  <  N  ->  L  <_  N )
)
7471, 73sylbid 215 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN0  /\  L  e.  NN0 )  -> 
( -.  N  <_  L  ->  L  <_  N
) )
7574ex 434 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN0  ->  ( L  e.  NN0  ->  ( -.  N  <_  L  ->  L  <_  N ) ) )
7666, 75syl5bi 217 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( (
# `  A )  e.  NN0  ->  ( -.  N  <_  L  ->  L  <_  N ) ) )
77763ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  (
( # `  A )  e.  NN0  ->  ( -.  N  <_  L  ->  L  <_  N ) ) )
7877imp32 433 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  ->  L  <_  N )
79 simpl3 1001 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  ->  N  <_  ( L  +  ( # `  B ) ) )
8078, 79jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  -> 
( L  <_  N  /\  N  <_  ( L  +  ( # `  B
) ) ) )
81 elfz2 11675 . . . . . . . . . . . . . 14  |-  ( N  e.  ( L ... ( L  +  ( # `
 B ) ) )  <->  ( ( L  e.  ZZ  /\  ( L  +  ( # `  B
) )  e.  ZZ  /\  N  e.  ZZ )  /\  ( L  <_  N  /\  N  <_  ( L  +  ( # `  B
) ) ) ) )
8264, 80, 81sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  /\  (
( # `  A )  e.  NN0  /\  -.  N  <_  L ) )  ->  N  e.  ( L ... ( L  +  (
# `  B )
) ) )
8382exp32 605 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  (
( # `  A )  e.  NN0  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `
 B ) ) ) ) ) )
8454, 83sylbi 195 . . . . . . . . . . 11  |-  ( N  e.  ( 0 ... ( L  +  (
# `  B )
) )  ->  (
( # `  A )  e.  NN0  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `
 B ) ) ) ) ) )
8584adantl 466 . . . . . . . . . 10  |-  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( ( # `  A
)  e.  NN0  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) ) )
864, 85syl5com 30 . . . . . . . . 9  |-  ( A  e. Word  V  ->  (
( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
8786adantr 465 . . . . . . . 8  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
8887imp 429 . . . . . . 7  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) )
8988a1dd 46 . . . . . 6  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  N  <_  L  ->  ( L  <_  M  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
90893imp 1190 . . . . 5  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  L  <_  M )  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) )
9153, 90jca 532 . . . 4  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  L  <_  M )  ->  ( M  e.  ( L ... N )  /\  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) )
929swrdccatin2 12671 . . . 4  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( L ... N
)  /\  N  e.  ( L ... ( L  +  ( # `  B
) ) ) )  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  ( B substr  <. ( M  -  L ) ,  ( N  -  L )
>. ) ) )
9325, 91, 92sylc 60 . . 3  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  L  <_  M )  ->  (
( A concat  B ) substr  <. M ,  N >. )  =  ( B substr  <. ( M  -  L ) ,  ( N  -  L ) >. )
)
94 simp1l 1020 . . . 4  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  -.  L  <_  M )  ->  ( A  e. Word  V  /\  B  e. Word  V ) )
95 nn0re 10800 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  NN0  ->  M  e.  RR )
9695adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  ->  M  e.  RR )
97 ltnle 9660 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  RR  /\  L  e.  RR )  ->  ( M  <  L  <->  -.  L  <_  M )
)
9896, 67, 97syl2anr 478 . . . . . . . . . . . . . . . . 17  |-  ( ( L  e.  NN0  /\  ( M  e.  NN0  /\  N  e.  NN0 )
)  ->  ( M  <  L  <->  -.  L  <_  M ) )
9998bicomd 201 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  NN0  /\  ( M  e.  NN0  /\  N  e.  NN0 )
)  ->  ( -.  L  <_  M  <->  M  <  L ) )
100 simpll 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN0  /\  L  e.  NN0 )  /\  M  <  L )  ->  M  e.  NN0 )
101 simplr 754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN0  /\  L  e.  NN0 )  /\  M  <  L )  ->  L  e.  NN0 )
102 ltle 9669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( M  e.  RR  /\  L  e.  RR )  ->  ( M  <  L  ->  M  <_  L )
)
10395, 67, 102syl2an 477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  e.  NN0  /\  L  e.  NN0 )  -> 
( M  <  L  ->  M  <_  L )
)
104103imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN0  /\  L  e.  NN0 )  /\  M  <  L )  ->  M  <_  L
)
105 elfz2nn0 11764 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  ( 0 ... L )  <->  ( M  e.  NN0  /\  L  e. 
NN0  /\  M  <_  L ) )
106100, 101, 104, 105syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN0  /\  L  e.  NN0 )  /\  M  <  L )  ->  M  e.  ( 0 ... L ) )
107106ex 434 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  e.  NN0  /\  L  e.  NN0 )  -> 
( M  <  L  ->  M  e.  ( 0 ... L ) ) )
108107ex 434 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN0  ->  ( L  e.  NN0  ->  ( M  <  L  ->  M  e.  ( 0 ... L
) ) ) )
109108adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  -> 
( L  e.  NN0  ->  ( M  <  L  ->  M  e.  ( 0 ... L ) ) ) )
110109impcom 430 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  NN0  /\  ( M  e.  NN0  /\  N  e.  NN0 )
)  ->  ( M  <  L  ->  M  e.  ( 0 ... L
) ) )
11199, 110sylbid 215 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  NN0  /\  ( M  e.  NN0  /\  N  e.  NN0 )
)  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L
) ) )
112111expcom 435 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  -> 
( L  e.  NN0  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L ) ) ) )
1131123adant3 1016 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN0  /\  N  e.  NN0  /\  M  <_  N )  ->  ( L  e.  NN0  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L ) ) ) )
11427, 113sylbi 195 . . . . . . . . . . . 12  |-  ( M  e.  ( 0 ... N )  ->  ( L  e.  NN0  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L ) ) ) )
11566, 114syl5bi 217 . . . . . . . . . . 11  |-  ( M  e.  ( 0 ... N )  ->  (
( # `  A )  e.  NN0  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L ) ) ) )
116115adantr 465 . . . . . . . . . 10  |-  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( ( # `  A
)  e.  NN0  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L ) ) ) )
1174, 116syl5com 30 . . . . . . . . 9  |-  ( A  e. Word  V  ->  (
( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L
) ) ) )
118117adantr 465 . . . . . . . 8  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L
) ) ) )
119118imp 429 . . . . . . 7  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L
) ) )
120119a1d 25 . . . . . 6  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  N  <_  L  ->  ( -.  L  <_  M  ->  M  e.  ( 0 ... L ) ) ) )
1211203imp 1190 . . . . 5  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  -.  L  <_  M )  ->  M  e.  ( 0 ... L
) )
122683ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  N  e.  RR )
12369bicomd 201 . . . . . . . . . . . . . . . . 17  |-  ( ( L  e.  RR  /\  N  e.  RR )  ->  ( -.  N  <_  L 
<->  L  <  N ) )
12467, 122, 123syl2an 477 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  -> 
( -.  N  <_  L 
<->  L  <  N ) )
12528adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  ->  L  e.  ZZ )
12660adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  -> 
( L  +  (
# `  B )
)  e.  ZZ )
12762adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  ->  N  e.  ZZ )
128125, 126, 1273jca 1176 . . . . . . . . . . . . . . . . . . 19  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  -> 
( L  e.  ZZ  /\  ( L  +  (
# `  B )
)  e.  ZZ  /\  N  e.  ZZ )
)
129128adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  /\  L  <  N )  -> 
( L  e.  ZZ  /\  ( L  +  (
# `  B )
)  e.  ZZ  /\  N  e.  ZZ )
)
13067, 122, 72syl2an 477 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  -> 
( L  <  N  ->  L  <_  N )
)
131130imp 429 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  /\  L  <  N )  ->  L  <_  N )
132 simp3 998 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  N  <_  ( L  +  (
# `  B )
) )
133132ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  /\  L  <  N )  ->  N  <_  ( L  +  ( # `  B ) ) )
134131, 133jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  /\  L  <  N )  -> 
( L  <_  N  /\  N  <_  ( L  +  ( # `  B
) ) ) )
135129, 134, 81sylanbrc 664 . . . . . . . . . . . . . . . . 17  |-  ( ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  /\  L  <  N )  ->  N  e.  ( L ... ( L  +  (
# `  B )
) ) )
136135ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  -> 
( L  <  N  ->  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) )
137124, 136sylbid 215 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  NN0  /\  ( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) ) )  -> 
( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) )
138137ex 434 . . . . . . . . . . . . . 14  |-  ( L  e.  NN0  ->  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  (
# `  B )
) ) ) ) )
13966, 138sylbi 195 . . . . . . . . . . . . 13  |-  ( (
# `  A )  e.  NN0  ->  ( ( N  e.  NN0  /\  ( L  +  ( # `  B
) )  e.  NN0  /\  N  <_  ( L  +  ( # `  B
) ) )  -> 
( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
1404, 139syl 16 . . . . . . . . . . . 12  |-  ( A  e. Word  V  ->  (
( N  e.  NN0  /\  ( L  +  (
# `  B )
)  e.  NN0  /\  N  <_  ( L  +  ( # `  B ) ) )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  (
# `  B )
) ) ) ) )
141140adantr 465 . . . . . . . . . . 11  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( N  e. 
NN0  /\  ( L  +  ( # `  B
) )  e.  NN0  /\  N  <_  ( L  +  ( # `  B
) ) )  -> 
( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
142141com12 31 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( L  +  ( # `
 B ) )  e.  NN0  /\  N  <_ 
( L  +  (
# `  B )
) )  ->  (
( A  e. Word  V  /\  B  e. Word  V )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
14354, 142sylbi 195 . . . . . . . . 9  |-  ( N  e.  ( 0 ... ( L  +  (
# `  B )
) )  ->  (
( A  e. Word  V  /\  B  e. Word  V )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
144143adantl 466 . . . . . . . 8  |-  ( ( M  e.  ( 0 ... N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) )  -> 
( ( A  e. Word  V  /\  B  e. Word  V
)  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) ) )
145144impcom 430 . . . . . . 7  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  N  <_  L  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) ) )
146145a1dd 46 . . . . . 6  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( -.  N  <_  L  ->  ( -.  L  <_  M  ->  N  e.  ( L ... ( L  +  (
# `  B )
) ) ) ) )
1471463imp 1190 . . . . 5  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  -.  L  <_  M )  ->  N  e.  ( L ... ( L  +  ( # `  B
) ) ) )
148121, 147jca 532 . . . 4  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  -.  L  <_  M )  ->  ( M  e.  ( 0 ... L )  /\  N  e.  ( L ... ( L  +  (
# `  B )
) ) ) )
1499swrdccatin12 12675 . . . 4  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... L
)  /\  N  e.  ( L ... ( L  +  ( # `  B
) ) ) )  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat  ( B substr  <.
0 ,  ( N  -  L ) >.
) ) ) )
15094, 148, 149sylc 60 . . 3  |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V
)  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  /\  -.  N  <_  L  /\  -.  L  <_  M )  ->  (
( A concat  B ) substr  <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat 
( B substr  <. 0 ,  ( N  -  L
) >. ) ) )
15124, 93, 1502if2 3987 . 2  |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) ) )  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  if ( N  <_  L ,  ( A substr  <. M ,  N >. ) ,  if ( L  <_  M , 
( B substr  <. ( M  -  L ) ,  ( N  -  L
) >. ) ,  ( ( A substr  <. M ,  L >. ) concat  ( B substr  <.
0 ,  ( N  -  L ) >.
) ) ) ) )
152151ex 434 1  |-  ( ( A  e. Word  V  /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ... N
)  /\  N  e.  ( 0 ... ( L  +  ( # `  B
) ) ) )  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  if ( N  <_  L ,  ( A substr  <. M ,  N >. ) ,  if ( L  <_  M , 
( B substr  <. ( M  -  L ) ,  ( N  -  L
) >. ) ,  ( ( A substr  <. M ,  L >. ) concat  ( B substr  <.
0 ,  ( N  -  L ) >.
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   ifcif 3939   <.cop 4033   class class class wbr 4447   ` cfv 5586  (class class class)co 6282   RRcr 9487   0cc0 9488    + caddc 9491    < clt 9624    <_ cle 9625    - cmin 9801   NN0cn0 10791   ZZcz 10860   ...cfz 11668   #chash 12369  Word cword 12496   concat cconcat 12498   substr csubstr 12500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-card 8316  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-n0 10792  df-z 10861  df-uz 11079  df-fz 11669  df-fzo 11789  df-hash 12370  df-word 12504  df-concat 12506  df-substr 12508
This theorem is referenced by:  swrdccat  12677  swrdccat3a  12678  swrdccat3b  12680
  Copyright terms: Public domain W3C validator