Metamath Proof Explorer

Theorem upwordnul

Description: Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024)

Ref Expression
Assertion upwordnul 
|- (/) e. UpWord S

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 elab6g 
 |-  ( (/) e. _V -> ( (/) e. { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } <-> A. w ( w = (/) -> ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) ) ) )
3 1 2 ax-mp 
 |-  ( (/) e. { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } <-> A. w ( w = (/) -> ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) ) )
4 wrd0 
 |-  (/) e. Word S
5 eleq1a 
 |-  ( (/) e. Word S -> ( w = (/) -> w e. Word S ) )
6 4 5 ax-mp 
 |-  ( w = (/) -> w e. Word S )
7 fveq2 
 |-  ( w = (/) -> ( # ` w ) = ( # ` (/) ) )
8 hash0 
 |-  ( # ` (/) ) = 0
9 7 8 eqtrdi 
 |-  ( w = (/) -> ( # ` w ) = 0 )
10 9 oveq1d 
 |-  ( w = (/) -> ( ( # ` w ) - 1 ) = ( 0 - 1 ) )
11 0red 
 |-  ( w = (/) -> 0 e. RR )
12 11 lem1d 
 |-  ( w = (/) -> ( 0 - 1 ) <_ 0 )
13 10 12 eqbrtrd 
 |-  ( w = (/) -> ( ( # ` w ) - 1 ) <_ 0 )
14 0z 
 |-  0 e. ZZ
15 9 14 eqeltrdi 
 |-  ( w = (/) -> ( # ` w ) e. ZZ )
16 1zzd 
 |-  ( w = (/) -> 1 e. ZZ )
17 15 16 zsubcld 
 |-  ( w = (/) -> ( ( # ` w ) - 1 ) e. ZZ )
18 fzon 
 |-  ( ( 0 e. ZZ /\ ( ( # ` w ) - 1 ) e. ZZ ) -> ( ( ( # ` w ) - 1 ) <_ 0 <-> ( 0 ..^ ( ( # ` w ) - 1 ) ) = (/) ) )
19 14 17 18 sylancr 
 |-  ( w = (/) -> ( ( ( # ` w ) - 1 ) <_ 0 <-> ( 0 ..^ ( ( # ` w ) - 1 ) ) = (/) ) )
20 13 19 mpbid 
 |-  ( w = (/) -> ( 0 ..^ ( ( # ` w ) - 1 ) ) = (/) )
21 rzal 
 |-  ( ( 0 ..^ ( ( # ` w ) - 1 ) ) = (/) -> A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) )
22 20 21 syl 
 |-  ( w = (/) -> A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) )
23 6 22 jca 
 |-  ( w = (/) -> ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) )
24 3 23 mpgbir 
 |-  (/) e. { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) }
25 df-upword 
 |-  UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) }
26 24 25 eleqtrri 
 |-  (/) e. UpWord S