Metamath Proof Explorer

Theorem uhgrwkspthlem1

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

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
3 wrdl1exs1 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ ( # ` F ) = 1 ) -> E. i e. dom ( iEdg ` G ) F = <" i "> )
4 funcnvs1 
 |-  Fun `' <" i ">
5 cnveq 
 |-  ( F = <" i "> -> `' F = `' <" i "> )
6 5 funeqd 
 |-  ( F = <" i "> -> ( Fun `' F <-> Fun `' <" i "> ) )
7 4 6 mpbiri 
 |-  ( F = <" i "> -> Fun `' F )
8 7 rexlimivw 
 |-  ( E. i e. dom ( iEdg ` G ) F = <" i "> -> Fun `' F )
9 3 8 syl 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ ( # ` F ) = 1 ) -> Fun `' F )
10 2 9 sylan 
 |-  ( ( F ( Walks ` G ) P /\ ( # ` F ) = 1 ) -> Fun `' F )