Theorem upgrspthswlk

Description: The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p_0, p_1, p_2 } be a hyperedge, then ( p_0, e, p_1, e, p_2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021) (Proof shortened by AV, 17-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	upgrspthswlk	⊢ ( 𝐺 ∈ UPGraph → ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } )

Proof

Step	Hyp	Ref	Expression
1		spthsfval	⊢ ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) }
2		istrl	⊢ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑓 ) )
3		upgrwlkdvde	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) → Fun ◡ 𝑓 )
4	3	3exp	⊢ ( 𝐺 ∈ UPGraph → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( Fun ◡ 𝑝 → Fun ◡ 𝑓 ) ) )
5	4	com23	⊢ ( 𝐺 ∈ UPGraph → ( Fun ◡ 𝑝 → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → Fun ◡ 𝑓 ) ) )
6	5	imp	⊢ ( ( 𝐺 ∈ UPGraph ∧ Fun ◡ 𝑝 ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → Fun ◡ 𝑓 ) )
7	6	pm4.71d	⊢ ( ( 𝐺 ∈ UPGraph ∧ Fun ◡ 𝑝 ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑓 ) ) )
8	2 7	bitr4id	⊢ ( ( 𝐺 ∈ UPGraph ∧ Fun ◡ 𝑝 ) → ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ↔ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) )
9	8	ex	⊢ ( 𝐺 ∈ UPGraph → ( Fun ◡ 𝑝 → ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ↔ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) ) )
10	9	pm5.32rd	⊢ ( 𝐺 ∈ UPGraph → ( ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) ) )
11	10	opabbidv	⊢ ( 𝐺 ∈ UPGraph → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } )
12	1 11	syl5eq	⊢ ( 𝐺 ∈ UPGraph → ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } )