Metamath Proof Explorer

Theorem wlkiswwlks2lem4

Description: Lemma 4 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-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 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 ) ) } ) )

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 wlkiswwlks2lem1 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
4 3 3adant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
5 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
6 5 3ad2ant2 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` P ) e. NN0 )
7 1 wlkiswwlks2lem2 
 |-  ( ( ( # ` P ) e. NN0 /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( F ` i ) = ( `' E ` { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
8 6 7 sylan 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( F ` i ) = ( `' E ` { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
9 8 adantr 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) /\ { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( F ` i ) = ( `' E ` { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
10 9 fveq2d 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) /\ { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( E ` ( F ` i ) ) = ( E ` ( `' E ` { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
11 2 uspgrf1oedg 
 |-  ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )
12 2 rneqi 
 |-  ran E = ran ( iEdg ` G )
13 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
14 12 13 eqtr4i 
 |-  ran E = ( Edg ` G )
15 f1oeq3 
 |-  ( ran E = ( Edg ` G ) -> ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) ) )
16 14 15 ax-mp 
 |-  ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) )
17 11 16 sylibr 
 |-  ( G e. USPGraph -> E : dom E -1-1-onto-> ran E )
18 17 3ad2ant1 
 |-  ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> E : dom E -1-1-onto-> ran E )
19 18 adantr 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> E : dom E -1-1-onto-> ran E )
20 f1ocnvfv2 
 |-  ( ( E : dom E -1-1-onto-> ran E /\ { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( E ` ( `' E ` { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
21 19 20 sylan 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) /\ { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( E ` ( `' E ` { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
22 10 21 eqtrd 
 |-  ( ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) /\ { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) -> ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
23 22 ex 
 |-  ( ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
24 23 ralimdva 
 |-  ( ( 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 ..^ ( ( # ` P ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
25 oveq2 
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) )
26 25 raleqdv 
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
27 26 imbi2d 
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( ( 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 ) ) } ) <-> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
28 24 27 syl5ibr 
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( ( 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 ) ) } ) ) )
29 4 28 mpcom 
 |-  ( ( 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 ) ) } ) )