Metamath Proof Explorer

Theorem usgr2wlkspthlem1

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

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

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 fvexd 
 |-  ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( F ` 0 ) e. _V )
9 fvexd 
 |-  ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( F ` 1 ) e. _V )
10 simpr 
 |-  ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( F ` 0 ) =/= ( F ` 1 ) )
11 8 9 10 3jca 
 |-  ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( ( F ` 0 ) e. _V /\ ( F ` 1 ) e. _V /\ ( F ` 0 ) =/= ( F ` 1 ) ) )
12 funcnvs2 
 |-  ( ( ( F ` 0 ) e. _V /\ ( F ` 1 ) e. _V /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> Fun `' <" ( F ` 0 ) ( F ` 1 ) "> )
13 7 11 12 3syl 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' <" ( F ` 0 ) ( F ` 1 ) "> )
14 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
15 14 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
16 simp2 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( # ` F ) = 2 )
17 wrdlen2s2 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ ( # ` F ) = 2 ) -> F = <" ( F ` 0 ) ( F ` 1 ) "> )
18 15 16 17 syl2an 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> F = <" ( F ` 0 ) ( F ` 1 ) "> )
19 18 cnveqd 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> `' F = `' <" ( F ` 0 ) ( F ` 1 ) "> )
20 19 funeqd 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( Fun `' F <-> Fun `' <" ( F ` 0 ) ( F ` 1 ) "> ) )
21 13 20 mpbird 
 |-  ( ( F ( Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' F )