Metamath Proof Explorer

Theorem wlkiswwlks2lem5

Description: Lemma 5 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 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 ) )

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 2 uspgrf1oedg 
 |-  ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )
4 2 rneqi 
 |-  ran E = ran ( iEdg ` G )
5 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
6 4 5 eqtr4i 
 |-  ran E = ( Edg ` G )
7 6 a1i 
 |-  ( G e. USPGraph -> ran E = ( Edg ` G ) )
8 7 f1oeq3d 
 |-  ( G e. USPGraph -> ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) ) )
9 3 8 mpbird 
 |-  ( G e. USPGraph -> E : dom E -1-1-onto-> ran E )
10 9 3ad2ant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> E : dom E -1-1-onto-> ran E )
11 10 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> E : dom E -1-1-onto-> ran E )
12 simpr 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
13 fveq2 
 |-  ( i = x -> ( P ` i ) = ( P ` x ) )
14 fvoveq1 
 |-  ( i = x -> ( P ` ( i + 1 ) ) = ( P ` ( x + 1 ) ) )
15 13 14 preq12d 
 |-  ( i = x -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( P ` x ) , ( P ` ( x + 1 ) ) } )
16 15 eleq1d 
 |-  ( i = x -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
17 16 adantl 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) /\ i = x ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
18 12 17 rspcdv 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
19 18 impancom 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
20 19 imp 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E )
21 f1ocnvdm 
 |-  ( ( E : dom E -1-1-onto-> ran E /\ { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) -> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E )
22 11 20 21 syl2anc 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E )
23 22 1 fmptd 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> F : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom E )
24 iswrdi 
 |-  ( F : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom E -> F e. Word dom E )
25 23 24 syl 
 |-  ( ( ( 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 )
26 25 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 ) )