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 fz01pr 
 |-  ( 0 ... 1 ) = { 0 , 1 }
5 3 4 eqtrdi 
 |-  ( ( # ` F ) = 1 -> ( 0 ... ( # ` F ) ) = { 0 , 1 } )
6 5 feq2d 
 |-  ( ( # ` F ) = 1 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) <-> P : { 0 , 1 } --> ( Vtx ` G ) ) )
7 6 adantr 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) <-> P : { 0 , 1 } --> ( Vtx ` G ) ) )
8 simpl 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` 0 ) = A )
9 simpr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = B )
10 8 9 neeq12d 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> A =/= B ) )
11 10 bicomd 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
12 fveq2 
 |-  ( ( # ` F ) = 1 -> ( P ` ( # ` F ) ) = ( P ` 1 ) )
13 12 neeq2d 
 |-  ( ( # ` F ) = 1 -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
14 11 13 sylan9bbr 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( A =/= B <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
15 7 14 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 ) ) ) )
16 0z 
 |-  0 e. ZZ
17 1z 
 |-  1 e. ZZ
18 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 ) >. } ) ) )
19 16 17 18 mp2an 
 |-  ( P : { 0 , 1 } --> ( Vtx ` G ) <-> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) )
20 funcnvs2 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) "> )
21 20 3expa 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) "> )
22 21 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 ) "> )
23 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 ) >. } )
24 s2prop 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) -> <" ( P ` 0 ) ( P ` 1 ) "> = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } )
25 24 eqcomd 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) -> { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } = <" ( P ` 0 ) ( P ` 1 ) "> )
26 25 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 ) "> )
27 26 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 ) "> )
28 23 27 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 ) "> )
29 28 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 ) "> )
30 29 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 ) "> ) )
31 22 30 mpbird 
 |-  ( ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } /\ ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) ) -> Fun `' P )
32 31 exp32 
 |-  ( P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) ) )
33 32 impcom 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) )
34 33 3impa 
 |-  ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` 1 ) e. ( Vtx ` G ) /\ P = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) )
35 19 34 sylbi 
 |-  ( P : { 0 , 1 } --> ( Vtx ` G ) -> ( ( P ` 0 ) =/= ( P ` 1 ) -> Fun `' P ) )
36 35 imp 
 |-  ( ( P : { 0 , 1 } --> ( Vtx ` G ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> Fun `' P )
37 15 36 biimtrdi 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A =/= B ) -> Fun `' P ) )
38 37 expd 
 |-  ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( A =/= B -> Fun `' P ) ) )
39 38 com12 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( # ` F ) = 1 /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( A =/= B -> Fun `' P ) ) )
40 39 expd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` F ) = 1 -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A =/= B -> Fun `' P ) ) ) )
41 40 com34 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` F ) = 1 -> ( A =/= B -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> Fun `' P ) ) ) )
42 41 impd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( # ` F ) = 1 /\ A =/= B ) -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> Fun `' P ) ) )
43 2 42 syl 
 |-  ( F ( Walks ` G ) P -> ( ( ( # ` F ) = 1 /\ A =/= B ) -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> Fun `' P ) ) )
44 43 3imp 
 |-  ( ( F ( Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P )