Theorem spthonprop

Description: Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 16-Jan-2021)

	Ref	Expression
Hypothesis	pthsonfval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	spthonprop	⊢ ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pthsonfval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	isspthson	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )
3	2	3adantl1	⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )
4		df-spthson	⊢ SPathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( SPaths ‘ 𝑔 ) 𝑝 ) } ) )
5		spthiswlk	⊢ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
6	5	adantl	⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑓 ( SPaths ‘ 𝐺 ) 𝑝 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
7	1 3 4 6	wksonproplem	⊢ ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )