This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ispthson

Description: Properties of a pair of functions to be a path between two given vertices. (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 ispthson ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 pthsonfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 pthsonfval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) } )
3 2 breqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) } 𝑃 ) )
4 breq12 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ↔ 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) )
5 breq12 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ↔ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) )
6 4 5 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )
7 eqid ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) }
8 6 7 brabga ⊢ ( ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ∧ 𝑓 ( Paths ‘ 𝐺 ) 𝑝 ) } 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )
9 3 8 sylan9bb ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) )