Metamath Proof Explorer

Theorem 2trlond

Description: A trail of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 30-Jan-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
2trld.n ⊢ φ → J ≠ K
Assertion 2trlond ⊢ φ → F A TrailsOn ⁡ G C 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 2trld.n ⊢ φ → J ≠ K
9 1 2 3 4 5 6 7 2wlkond ⊢ φ → F A WalksOn ⁡ G C P
10 1 2 3 4 5 6 7 8 2trld ⊢ φ → F Trails ⁡ G P
11 3 simp1d ⊢ φ → A ∈ V
12 3 simp3d ⊢ φ → C ∈ V
13 s2cli ⊢ ⟨“ JK ”⟩ ∈ Word V
14 2 13 eqeltri ⊢ F ∈ Word V
15 14 a1i ⊢ φ → F ∈ Word V
16 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
17 1 16 eqeltri ⊢ P ∈ Word V
18 17 a1i ⊢ φ → P ∈ Word V
19 6 istrlson ⊢ A ∈ V ∧ C ∈ V ∧ F ∈ Word V ∧ P ∈ Word V → F A TrailsOn ⁡ G C P ↔ F A WalksOn ⁡ G C P ∧ F Trails ⁡ G P
20 11 12 15 18 19 syl22anc ⊢ φ → F A TrailsOn ⁡ G C P ↔ F A WalksOn ⁡ G C P ∧ F Trails ⁡ G P
21 9 10 20 mpbir2and ⊢ φ → F A TrailsOn ⁡ G C P