Metamath Proof Explorer

Theorem wlk2v2elem2

Description: Lemma 2 for wlk2v2e : The values of I after F are edges between two vertices enumerated by P . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)

Ref Expression
Hypotheses wlk2v2e.i 
|- I = <" { X , Y } ">
wlk2v2e.f 
|- F = <" 0 0 ">
wlk2v2e.x 
|- X e. _V
wlk2v2e.y 
|- Y e. _V
wlk2v2e.p 
|- P = <" X Y X ">
Assertion wlk2v2elem2 
|- A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) }

Proof

Step Hyp Ref Expression
1 wlk2v2e.i 
 |-  I = <" { X , Y } ">
2 wlk2v2e.f 
 |-  F = <" 0 0 ">
3 wlk2v2e.x 
 |-  X e. _V
4 wlk2v2e.y 
 |-  Y e. _V
5 wlk2v2e.p 
 |-  P = <" X Y X ">
6 2 fveq1i 
 |-  ( F ` 0 ) = ( <" 0 0 "> ` 0 )
7 0z 
 |-  0 e. ZZ
8 s2fv0 
 |-  ( 0 e. ZZ -> ( <" 0 0 "> ` 0 ) = 0 )
9 7 8 ax-mp 
 |-  ( <" 0 0 "> ` 0 ) = 0
10 6 9 eqtri 
 |-  ( F ` 0 ) = 0
11 10 fveq2i 
 |-  ( I ` ( F ` 0 ) ) = ( I ` 0 )
12 1 fveq1i 
 |-  ( I ` 0 ) = ( <" { X , Y } "> ` 0 )
13 prex 
 |-  { X , Y } e. _V
14 s1fv 
 |-  ( { X , Y } e. _V -> ( <" { X , Y } "> ` 0 ) = { X , Y } )
15 13 14 ax-mp 
 |-  ( <" { X , Y } "> ` 0 ) = { X , Y }
16 12 15 eqtri 
 |-  ( I ` 0 ) = { X , Y }
17 5 fveq1i 
 |-  ( P ` 0 ) = ( <" X Y X "> ` 0 )
18 s3fv0 
 |-  ( X e. _V -> ( <" X Y X "> ` 0 ) = X )
19 3 18 ax-mp 
 |-  ( <" X Y X "> ` 0 ) = X
20 17 19 eqtri 
 |-  ( P ` 0 ) = X
21 5 fveq1i 
 |-  ( P ` 1 ) = ( <" X Y X "> ` 1 )
22 s3fv1 
 |-  ( Y e. _V -> ( <" X Y X "> ` 1 ) = Y )
23 4 22 ax-mp 
 |-  ( <" X Y X "> ` 1 ) = Y
24 21 23 eqtri 
 |-  ( P ` 1 ) = Y
25 20 24 preq12i 
 |-  { ( P ` 0 ) , ( P ` 1 ) } = { X , Y }
26 25 eqcomi 
 |-  { X , Y } = { ( P ` 0 ) , ( P ` 1 ) }
27 11 16 26 3eqtri 
 |-  ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) }
28 2 fveq1i 
 |-  ( F ` 1 ) = ( <" 0 0 "> ` 1 )
29 s2fv1 
 |-  ( 0 e. ZZ -> ( <" 0 0 "> ` 1 ) = 0 )
30 7 29 ax-mp 
 |-  ( <" 0 0 "> ` 1 ) = 0
31 28 30 eqtri 
 |-  ( F ` 1 ) = 0
32 31 fveq2i 
 |-  ( I ` ( F ` 1 ) ) = ( I ` 0 )
33 prcom 
 |-  { X , Y } = { Y , X }
34 5 fveq1i 
 |-  ( P ` 2 ) = ( <" X Y X "> ` 2 )
35 s3fv2 
 |-  ( X e. _V -> ( <" X Y X "> ` 2 ) = X )
36 3 35 ax-mp 
 |-  ( <" X Y X "> ` 2 ) = X
37 34 36 eqtri 
 |-  ( P ` 2 ) = X
38 24 37 preq12i 
 |-  { ( P ` 1 ) , ( P ` 2 ) } = { Y , X }
39 38 eqcomi 
 |-  { Y , X } = { ( P ` 1 ) , ( P ` 2 ) }
40 33 39 eqtri 
 |-  { X , Y } = { ( P ` 1 ) , ( P ` 2 ) }
41 32 16 40 3eqtri 
 |-  ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) }
42 2wlklem 
 |-  ( A. k e. { 0 , 1 } ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
43 27 41 42 mpbir2an 
 |-  A. k e. { 0 , 1 } ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) }
44 5 2 2wlkdlem2 
 |-  ( 0 ..^ ( # ` F ) ) = { 0 , 1 }
45 44 raleqi 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> A. k e. { 0 , 1 } ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
46 43 45 mpbir 
 |-  A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) }