Metamath Proof Explorer

Theorem uhgrwkspthlem2

Description: Lemma 2 for uhgrwkspth . (Contributed by AV, 25-Jan-2021)

Ref Expression
Assertion uhgrwkspthlem2 
|- ( ( F ( Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
3 oveq2 
 |-  ( ( # ` F ) = 1 -> ( 0 ... ( # ` F ) ) = ( 0 ... 1 ) )
4 1e0p1 
 |-  1 = ( 0 + 1 )
5 4 oveq2i 
 |-  ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
6 0z 
 |-  0 e. ZZ
7 fzpr 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
8 6 7 ax-mp 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
9 0p1e1 
 |-  ( 0 + 1 ) = 1
10 9 preq2i 
 |-  { 0 , ( 0 + 1 ) } = { 0 , 1 }
11 5 8 10 3eqtri 
 |-  ( 0 ... 1 ) = { 0 , 1 }
12 3 11 eqtrdi 
 |-  ( ( # ` F ) = 1 -> ( 0 ... ( # ` F ) ) = { 0 , 1 } )
13 12 feq2d 
 |-  ( ( # ` F ) = 1 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) <-> P : { 0 , 1 } --> ( Vtx ` G ) ) )
14 13 adantr 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) <-> P : { 0 , 1 } --> ( Vtx ` G ) ) )
15 simpl 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` 0 ) = A )
16 simpr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = B )
17 15 16 neeq12d 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> A =/= B ) )
18 17 bicomd 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
19 fveq2 
 |-  ( ( # ` F ) = 1 -> ( P ` ( # ` F ) ) = ( P ` 1 ) )
20 19 neeq2d 
 |-  ( ( # ` F ) = 1 -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
21 18 20 sylan9bbr 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
22 14 21 anbi12d 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A =/= B ) <-> ( P : { 0 , 1 } --> ( Vtx ` G ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) )
23 1z 
 |-  1 e. ZZ
24 fpr2g 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( P : { 0 , 1 } --> ( Vtx ` G ) <-> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) ) )
25 6 23 24 mp2an 
 |-  ( P : { 0 , 1 } --> ( Vtx ` G ) <-> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) )
26 funcnvs2 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) "> )
27 26 3expa 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) "> )
28 27 adantl 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) "> )
29 simpl 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } )
30 s2prop 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) -> <" ( P ` 0 ) ( P ` 1 ) "> = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } )
31 30 eqcomd 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) -> { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } = <" ( P ` 0 ) ( P ` 1 ) "> )
32 31 adantr 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } = <" ( P ` 0 ) ( P ` 1 ) "> )
33 32 adantl 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } = <" ( P ` 0 ) ( P ` 1 ) "> )
34 29 33 eqtrd 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> P = <" ( P ` 0 ) ( P ` 1 ) "> )
35 34 cnveqd 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> `' P = `' <" ( P ` 0 ) ( P ` 1 ) "> )
36 35 funeqd 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> ( Fun `' P <-> Fun `' <" ( P ` 0 ) ( P ` 1 ) "> ) )
37 28 36 mpbird 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> Fun `' P )
38 37 exp32 
 |-  ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) ) )
39 38 impcom 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) )
40 39 3impa 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) )
41 25 40 sylbi 
 |-  ( P : { 0 , 1 } --> ( Vtx ` G ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) )
42 41 imp 
 |-  ( ( P : { 0 , 1 } --> ( Vtx ` G ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> Fun `' P )
43 22 42 syl6bi 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A =/= B ) -> Fun `' P ) )
44 43 expd 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( A =/= B -> Fun `' P ) ) )
45 44 com12 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( A =/= B -> Fun `' P ) ) )
46 45 expd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` F ) = 1 -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A =/= B -> Fun `' P ) ) ) )
47 46 com34 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` F ) = 1 -> ( A =/= B -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> Fun `' P ) ) ) )
48 47 impd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( # ` F ) = 1 /\ A =/= B ) -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> Fun `' P ) ) )
49 2 48 syl 
 |-  ( F ( Walks ` G ) P -> ( ( ( # ` F ) = 1 /\ A =/= B ) -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> Fun `' P ) ) )
50 49 3imp 
 |-  ( ( F ( Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P )