Metamath Proof Explorer

Theorem iswlkg

Description: Generalization of iswlk : Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-Jan-2021)

Ref Expression
Hypotheses iswlkg.v ⊢ V = Vtx ⁡ G
iswlkg.i ⊢ I = iEdg ⁡ G
Assertion iswlkg ⊢ G ∈ W → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 iswlkg.v ⊢ V = Vtx ⁡ G
2 iswlkg.i ⊢ I = iEdg ⁡ G
3 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
4 3simpc ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ V ∧ P ∈ V
5 3 4 syl ⊢ F Walks ⁡ G P → F ∈ V ∧ P ∈ V
6 5 a1i ⊢ G ∈ W → F Walks ⁡ G P → F ∈ V ∧ P ∈ V
7 elex ⊢ F ∈ Word dom ⁡ I → F ∈ V
8 ovex ⊢ 0 … F ∈ V
9 1 fvexi ⊢ V ∈ V
10 8 9 fpm ⊢ P : 0 … F ⟶ V → P ∈ V ↑ 𝑝𝑚 0 … F
11 10 elexd ⊢ P : 0 … F ⟶ V → P ∈ V
12 7 11 anim12i ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V → F ∈ V ∧ P ∈ V
13 12 3adant3 ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → F ∈ V ∧ P ∈ V
14 13 a1i ⊢ G ∈ W → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → F ∈ V ∧ P ∈ V
15 1 2 iswlk ⊢ G ∈ W ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
16 15 3expib ⊢ G ∈ W → F ∈ V ∧ P ∈ V → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
17 6 14 16 pm5.21ndd ⊢ G ∈ W → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k