Theorem trlf1

Description: The enumeration F of a trail <. F , P >. is injective. (Contributed by AV, 20-Feb-2021) (Proof shortened by AV, 29-Oct-2021)

	Ref	Expression
Hypothesis	trlf1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
Assertion	trlf1	$$⊢F\mathrm{Trails}\left(G\right)P\to F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I$$

Proof

Step	Hyp	Ref	Expression
1		trlf1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2		istrl	$$⊢F\mathrm{Trails}\left(G\right)P\leftrightarrow \left(F\mathrm{Walks}\left(G\right)P\wedge \mathrm{Fun}{F}^{-1}\right)$$
3	1	wlkf	$$⊢F\mathrm{Walks}\left(G\right)P\to F\in \mathrm{Word}\mathrm{dom}I$$
4		wrdf	$$⊢F\in \mathrm{Word}\mathrm{dom}I\to F:\left(0..^\left|F\right|\right)⟶\mathrm{dom}I$$
5		df-f1	$$⊢F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I\leftrightarrow \left(F:\left(0..^\left|F\right|\right)⟶\mathrm{dom}I\wedge \mathrm{Fun}{F}^{-1}\right)$$
6	5	simplbi2	$$⊢F:\left(0..^\left|F\right|\right)⟶\mathrm{dom}I\to \left(\mathrm{Fun}{F}^{-1}\to F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I\right)$$
7	3 4 6	3syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(\mathrm{Fun}{F}^{-1}\to F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I\right)$$
8	7	imp	$$⊢\left(F\mathrm{Walks}\left(G\right)P\wedge \mathrm{Fun}{F}^{-1}\right)\to F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I$$
9	2 8	sylbi	$$⊢F\mathrm{Trails}\left(G\right)P\to F:\left(0..^\left|F\right|\right)\underset{1-1}{⟶}\mathrm{dom}I$$