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

Metamath Proof Explorer

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 = iEdg ⁡ G
Assertion trlf1 ⊢ F Trails ⁡ G P → F : 0 ..^ F ⟶ 1-1 dom ⁡ I

Proof

Step Hyp Ref Expression
1 trlf1.i ⊢ I = iEdg ⁡ G
2 istrl ⊢ F Trails ⁡ G P ↔ F Walks ⁡ G P ∧ Fun ⁡ F -1
3 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
4 wrdf ⊢ F ∈ Word dom ⁡ I → F : 0 ..^ F ⟶ dom ⁡ I
5 df-f1 ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ I ↔ F : 0 ..^ F ⟶ dom ⁡ I ∧ Fun ⁡ F -1
6 5 simplbi2 ⊢ F : 0 ..^ F ⟶ dom ⁡ I → Fun ⁡ F -1 → F : 0 ..^ F ⟶ 1-1 dom ⁡ I
7 3 4 6 3syl ⊢ F Walks ⁡ G P → Fun ⁡ F -1 → F : 0 ..^ F ⟶ 1-1 dom ⁡ I
8 7 imp ⊢ F Walks ⁡ G P ∧ Fun ⁡ F -1 → F : 0 ..^ F ⟶ 1-1 dom ⁡ I
9 2 8 sylbi ⊢ F Trails ⁡ G P → F : 0 ..^ F ⟶ 1-1 dom ⁡ I