Metamath Proof Explorer

Theorem 2wlkd

Description: Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018) (Revised by AV, 23-Jan-2021) (Proof shortened by AV, 14-Feb-2021) (Revised by AV, 24-Mar-2021)

Ref Expression
Hypotheses 2wlkd.p ⊢ P = ⟨“ ABC ”⟩
2wlkd.f ⊢ F = ⟨“ JK ”⟩
2wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
2wlkd.n ⊢ φ → A ≠ B ∧ B ≠ C
2wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
2wlkd.v ⊢ V = Vtx ⁡ G
2wlkd.i ⊢ I = iEdg ⁡ G
Assertion 2wlkd ⊢ φ → F Walks ⁡ G P

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ P = ⟨“ ABC ”⟩
2 2wlkd.f ⊢ F = ⟨“ JK ”⟩
3 2wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
4 2wlkd.n ⊢ φ → A ≠ B ∧ B ≠ C
5 2wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
6 2wlkd.v ⊢ V = Vtx ⁡ G
7 2wlkd.i ⊢ I = iEdg ⁡ G
8 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
9 1 8 eqeltri ⊢ P ∈ Word V
10 9 a1i ⊢ φ → P ∈ Word V
11 s2cli ⊢ ⟨“ JK ”⟩ ∈ Word V
12 2 11 eqeltri ⊢ F ∈ Word V
13 12 a1i ⊢ φ → F ∈ Word V
14 1 2 2wlkdlem1 ⊢ P = F + 1
15 14 a1i ⊢ φ → P = F + 1
16 1 2 3 4 5 2wlkdlem10 ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
17 1 2 3 4 2wlkdlem5 ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
18 6 1vgrex ⊢ A ∈ V → G ∈ V
19 18 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → G ∈ V
20 3 19 syl ⊢ φ → G ∈ V
21 1 2 3 2wlkdlem4 ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V
22 10 13 15 16 17 20 6 7 21 wlkd ⊢ φ → F Walks ⁡ G P