Metamath Proof Explorer

Theorem upgrf1istrl

Description: Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Hypotheses upgrtrls.v ⊢ V = Vtx ⁡ G
upgrtrls.i ⊢ I = iEdg ⁡ G
Assertion upgrf1istrl ⊢ G ∈ UPGraph → F Trails ⁡ G P ↔ F : 0 ..^ F ⟶ 1-1 dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 upgrtrls.v ⊢ V = Vtx ⁡ G
2 upgrtrls.i ⊢ I = iEdg ⁡ G
3 1 2 upgristrl ⊢ G ∈ UPGraph → F Trails ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
4 iswrdb ⊢ F ∈ Word dom ⁡ I ↔ F : 0 ..^ F ⟶ dom ⁡ I
5 4 a1i ⊢ G ∈ UPGraph → F ∈ Word dom ⁡ I ↔ F : 0 ..^ F ⟶ dom ⁡ I
6 5 anbi1d ⊢ G ∈ UPGraph → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ↔ F : 0 ..^ F ⟶ dom ⁡ I ∧ Fun ⁡ F -1
7 df-f1 ⊢ F : 0 ..^ F ⟶ 1-1 dom ⁡ I ↔ F : 0 ..^ F ⟶ dom ⁡ I ∧ Fun ⁡ F -1
8 6 7 bitr4di ⊢ G ∈ UPGraph → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ↔ F : 0 ..^ F ⟶ 1-1 dom ⁡ I
9 8 3anbi1d ⊢ G ∈ UPGraph → F ∈ Word dom ⁡ I ∧ Fun ⁡ F -1 ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ↔ F : 0 ..^ F ⟶ 1-1 dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
10 3 9 bitrd ⊢ G ∈ UPGraph → F Trails ⁡ G P ↔ F : 0 ..^ F ⟶ 1-1 dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1