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 ‘ 𝐺 ) 𝑃 ) ) )