Theorem pthsonfval

Description: The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 16-Jan-2021) (Revised by AV, 21-Mar-2021)

	Ref	Expression
Hypothesis	pthsonfval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	pthsonfval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) } )

Proof

Step	Hyp	Ref	Expression
1		pthsonfval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	1vgrex	⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ V )
3	2	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
4		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
5	4 1	eleqtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
6		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
7	6 1	eleqtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
8		wksv	⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V
9	8	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V )
10		pthiswlk	⊢ ( 𝑓 ( Paths ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
11	10	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
12		df-pthson	⊢ PathsOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝑎 ( TrailsOn ‘ 𝑔 ) 𝑏 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ) } ) )
13	3 5 7 9 11 12	mptmpoopabovd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) } )