Metamath Proof Explorer

Theorem usgr2wlkspthlem2

Description: Lemma 2 for usgr2wlkspth . (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 27-Jan-2021)

Ref Expression
Assertion usgr2wlkspthlem2 
|- ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' P )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> G e. USGraph )
2 1 anim2i 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( F ( Walks ` G ) P /\ G e. USGraph ) )
3 2 ancomd 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( G e. USGraph /\ F ( Walks ` G ) P ) )
4 3simpc 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
5 4 adantl 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
6 usgr2wlkneq 
 |-  ( ( ( G e. USGraph /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) )
7 3 5 6 syl2anc 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) )
8 simpl 
 |-  ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) )
9 fvex 
 |-  ( P ` 0 ) e. _V
10 fvex 
 |-  ( P ` 1 ) e. _V
11 fvex 
 |-  ( P ` 2 ) e. _V
12 9 10 11 3pm3.2i 
 |-  ( ( P ` 0 ) e. _V /\ ( P ` 1 ) e. _V /\ ( P ` 2 ) e. _V )
13 8 12 jctil 
 |-  ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( ( ( P ` 0 ) e. _V /\ ( P ` 1 ) e. _V /\ ( P ` 2 ) e. _V ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) )
14 funcnvs3 
 |-  ( ( ( ( P ` 0 ) e. _V /\ ( P ` 1 ) e. _V /\ ( P ` 2 ) e. _V ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) ( P ` 2 ) "> )
15 7 13 14 3syl 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' <" ( P ` 0 ) ( P ` 1 ) ( P ` 2 ) "> )
16 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
17 16 wlkpwrd 
 |-  ( F ( Walks ` G ) P -> P e. Word ( Vtx ` G ) )
18 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
19 oveq1 
 |-  ( ( # ` F ) = 2 -> ( ( # ` F ) + 1 ) = ( 2 + 1 ) )
20 2p1e3 
 |-  ( 2 + 1 ) = 3
21 19 20 eqtrdi 
 |-  ( ( # ` F ) = 2 -> ( ( # ` F ) + 1 ) = 3 )
22 21 3ad2ant2 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( # ` F ) + 1 ) = 3 )
23 18 22 sylan9eq 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( # ` P ) = 3 )
24 wrdlen3s3 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = 3 ) -> P = <" ( P ` 0 ) ( P ` 1 ) ( P ` 2 ) "> )
25 17 23 24 syl2an2r 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> P = <" ( P ` 0 ) ( P ` 1 ) ( P ` 2 ) "> )
26 25 cnveqd 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> `' P = `' <" ( P ` 0 ) ( P ` 1 ) ( P ` 2 ) "> )
27 26 funeqd 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( Fun `' P <-> Fun `' <" ( P ` 0 ) ( P ` 1 ) ( P ` 2 ) "> ) )
28 15 27 mpbird 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' P )