This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkiswwlks2lem6

Description: Lemma 6 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Hypotheses wlkiswwlks2lem.f 
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
wlkiswwlks2lem.e 
|- E = ( iEdg ` G )
Assertion wlkiswwlks2lem6 
|- ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f 
 |-  F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
2 wlkiswwlks2lem.e 
 |-  E = ( iEdg ` G )
3 1 2 wlkiswwlks2lem5 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> F e. Word dom E ) )
4 3 imp 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> F e. Word dom E )
5 1 wlkiswwlks2lem3 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
6 5 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
7 6 adantr 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> P : ( 0 ... ( # ` F ) ) --> V )
8 1 2 wlkiswwlks2lem4 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
9 8 imp 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
10 4 7 9 3jca 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
11 10 ex 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )