This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ◡ 𝐹 )