Theorem istrlson

Description: Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 21-Mar-2021)

	Ref	Expression
Hypothesis	trlsonfval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	istrlson	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )

Proof

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