Theorem uhgrwkspthlem1

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

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

Proof

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