| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 2 |
1
|
spthonprop |
⊢ ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) ) |
| 3 |
|
3simpc |
⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 4 |
3
|
3anim1i |
⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) ) |
| 5 |
|
spthispth |
⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
| 6 |
5
|
anim2i |
⊢ ( ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) |
| 7 |
6
|
3ad2ant3 |
⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) |
| 8 |
1
|
ispthson |
⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
| 9 |
8
|
3adant3 |
⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
| 10 |
7 9
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) → 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) |
| 11 |
2 4 10
|
3syl |
⊢ ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) |