uhgrwkspthlem1

		Ref	Expression
	Assertion	uhgrwkspthlem1	$⊢ (F Walks (G) P \land \|F\| = 1) \to Fun F^{-1}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
3		wrdl1exs1	$⊢ (F \in Word dom iEdg (G) \land \|F\| = 1) \to \exists i \in dom iEdg (G) F = ⟨“ i ”⟩$
4		funcnvs1	$⊢ Fun {⟨“ i ”⟩}^{-1}$
5		cnveq	$⊢ F = ⟨“ i ”⟩ \to F^{-1} = {⟨“ i ”⟩}^{-1}$
6	5	funeqd	$⊢ F = ⟨“ i ”⟩ \to (Fun F^{-1} \leftrightarrow Fun {⟨“ i ”⟩}^{-1})$
7	4 6	mpbiri	$⊢ F = ⟨“ i ”⟩ \to Fun F^{-1}$
8	7	rexlimivw	$⊢ \exists i \in dom iEdg (G) F = ⟨“ i ”⟩ \to Fun F^{-1}$
9	3 8	syl	$⊢ (F \in Word dom iEdg (G) \land \|F\| = 1) \to Fun F^{-1}$
10	2 9	sylan	$⊢ (F Walks (G) P \land \|F\| = 1) \to Fun F^{-1}$

Metamath Proof Explorer