Metamath Proof Explorer

Theorem spthonpthon

Description: A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021)

Ref Expression
Assertion spthonpthon ⊢FASPathsOn⁡GBP→FAPathsOn⁡GBP

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 1 spthonprop ⊢FASPathsOn⁡GBP→G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FSPaths⁡GP
3 3simpc ⊢G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G→A∈Vtx⁡G∧B∈Vtx⁡G
4 3 3anim1i ⊢G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FSPaths⁡GP→A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FSPaths⁡GP
5 spthispth ⊢FSPaths⁡GP→FPaths⁡GP
6 5 anim2i ⊢FATrailsOn⁡GBP∧FSPaths⁡GP→FATrailsOn⁡GBP∧FPaths⁡GP
7 6 3ad2ant3 ⊢A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FSPaths⁡GP→FATrailsOn⁡GBP∧FPaths⁡GP
8 1 ispthson ⊢A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V→FAPathsOn⁡GBP↔FATrailsOn⁡GBP∧FPaths⁡GP
9 8 3adant3 ⊢A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FSPaths⁡GP→FAPathsOn⁡GBP↔FATrailsOn⁡GBP∧FPaths⁡GP
10 7 9 mpbird ⊢A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FATrailsOn⁡GBP∧FSPaths⁡GP→FAPathsOn⁡GBP
11 2 4 10 3syl ⊢FASPathsOn⁡GBP→FAPathsOn⁡GBP