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 ) ) } ) ) )