Metamath Proof Explorer

Theorem ewlkle

Description: An s-walk of edges is also a t-walk of edges if t <_ s . (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion ewlkle 
|- ( ( F e. ( G EdgWalks S ) /\ T e. NN0* /\ T <_ S ) -> F e. ( G EdgWalks T ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 ewlkprop 
 |-  ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
3 simpl2 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) /\ ( T e. NN0* /\ T <_ S ) ) -> F e. Word dom ( iEdg ` G ) )
4 xnn0xr 
 |-  ( T e. NN0* -> T e. RR* )
5 4 adantl 
 |-  ( ( S e. NN0* /\ T e. NN0* ) -> T e. RR* )
6 xnn0xr 
 |-  ( S e. NN0* -> S e. RR* )
7 6 adantr 
 |-  ( ( S e. NN0* /\ T e. NN0* ) -> S e. RR* )
8 fvex 
 |-  ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) e. _V
9 8 inex1 
 |-  ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) e. _V
10 hashxrcl 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) e. _V -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* )
11 9 10 mp1i 
 |-  ( ( S e. NN0* /\ T e. NN0* ) -> ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* )
12 xrletr 
 |-  ( ( T e. RR* /\ S e. RR* /\ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) e. RR* ) -> ( ( T <_ S /\ S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
13 5 7 11 12 syl3anc 
 |-  ( ( S e. NN0* /\ T e. NN0* ) -> ( ( T <_ S /\ S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
14 13 exp4b 
 |-  ( S e. NN0* -> ( T e. NN0* -> ( T <_ S -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) ) )
15 14 adantl 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( T e. NN0* -> ( T <_ S -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) ) )
16 15 imp32 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ ( T e. NN0* /\ T <_ S ) ) -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
17 16 ralimdv 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ ( T e. NN0* /\ T <_ S ) ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
18 17 ex 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( ( T e. NN0* /\ T <_ S ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) )
19 18 com23 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( T e. NN0* /\ T <_ S ) -> A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) )
20 19 a1d 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( F e. Word dom ( iEdg ` G ) -> ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( T e. NN0* /\ T <_ S ) -> A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) ) )
21 20 3imp1 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) /\ ( T e. NN0* /\ T <_ S ) ) -> A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
22 simpl1l 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) /\ ( T e. NN0* /\ T <_ S ) ) -> G e. _V )
23 simprl 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) /\ ( T e. NN0* /\ T <_ S ) ) -> T e. NN0* )
24 1 isewlk 
 |-  ( ( G e. _V /\ T e. NN0* /\ F e. Word dom ( iEdg ` G ) ) -> ( F e. ( G EdgWalks T ) <-> ( F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) )
25 22 23 3 24 syl3anc 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) /\ ( T e. NN0* /\ T <_ S ) ) -> ( F e. ( G EdgWalks T ) <-> ( F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) T <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) ) )
26 3 21 25 mpbir2and 
 |-  ( ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) /\ ( T e. NN0* /\ T <_ S ) ) -> F e. ( G EdgWalks T ) )
27 26 ex 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( F ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( ( T e. NN0* /\ T <_ S ) -> F e. ( G EdgWalks T ) ) )
28 2 27 syl 
 |-  ( F e. ( G EdgWalks S ) -> ( ( T e. NN0* /\ T <_ S ) -> F e. ( G EdgWalks T ) ) )
29 28 3impib 
 |-  ( ( F e. ( G EdgWalks S ) /\ T e. NN0* /\ T <_ S ) -> F e. ( G EdgWalks T ) )