Theorem uhgrwkspthlem1

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

	Ref	Expression
Assertion	uhgrwkspthlem1	⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 1 ) → Fun ◡ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
2	1	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
3		wrdl1exs1	⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐹 = ⟨“ 𝑖 ”⟩ )
4		funcnvs1	⊢ Fun ◡ ⟨“ 𝑖 ”⟩
5		cnveq	⊢ ( 𝐹 = ⟨“ 𝑖 ”⟩ → ◡ 𝐹 = ◡ ⟨“ 𝑖 ”⟩ )
6	5	funeqd	⊢ ( 𝐹 = ⟨“ 𝑖 ”⟩ → ( Fun ◡ 𝐹 ↔ Fun ◡ ⟨“ 𝑖 ”⟩ ) )
7	4 6	mpbiri	⊢ ( 𝐹 = ⟨“ 𝑖 ”⟩ → Fun ◡ 𝐹 )
8	7	rexlimivw	⊢ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐹 = ⟨“ 𝑖 ”⟩ → Fun ◡ 𝐹 )
9	3 8	syl	⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → Fun ◡ 𝐹 )
10	2 9	sylan	⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 1 ) → Fun ◡ 𝐹 )