Metamath Proof Explorer

Theorem 2pthond

Description: A simple path 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, 24-Jan-2021) (Proof shortened 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
2spthd.n ⊢ φ → A ≠ C
Assertion 2pthond ⊢ φ → F A SPathsOn ⁡ 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 2spthd.n ⊢ φ → A ≠ C
10 1 2 3 4 5 6 7 8 2trlond ⊢ φ → F A TrailsOn ⁡ G C P
11 1 2 3 4 5 6 7 8 9 2spthd ⊢ φ → F SPaths ⁡ G P
12 3simpb ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V ∧ C ∈ V
13 3 12 syl ⊢ φ → A ∈ V ∧ C ∈ V
14 s2cli ⊢ ⟨“ JK ”⟩ ∈ Word V
15 2 14 eqeltri ⊢ F ∈ Word V
16 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
17 1 16 eqeltri ⊢ P ∈ Word V
18 15 17 pm3.2i ⊢ F ∈ Word V ∧ P ∈ Word V
19 6 isspthson ⊢ A ∈ V ∧ C ∈ V ∧ F ∈ Word V ∧ P ∈ Word V → F A SPathsOn ⁡ G C P ↔ F A TrailsOn ⁡ G C P ∧ F SPaths ⁡ G P
20 13 18 19 sylancl ⊢ φ → F A SPathsOn ⁡ G C P ↔ F A TrailsOn ⁡ G C P ∧ F SPaths ⁡ G P
21 10 11 20 mpbir2and ⊢ φ → F A SPathsOn ⁡ G C P