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

Metamath Proof Explorer

Theorem istrl

Description: Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 28-Dec-2020) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion istrl ⊢ F Trails ⁡ G P ↔ F Walks ⁡ G P ∧ Fun ⁡ F -1

Proof

Step Hyp Ref Expression
1 trlsfval ⊢ Trails ⁡ G = f p | f Walks ⁡ G p ∧ Fun ⁡ f -1
2 cnveq ⊢ f = F → f -1 = F -1
3 2 funeqd ⊢ f = F → Fun ⁡ f -1 ↔ Fun ⁡ F -1
4 3 adantr ⊢ f = F ∧ p = P → Fun ⁡ f -1 ↔ Fun ⁡ F -1
5 relwlk ⊢ Rel ⁡ Walks ⁡ G
6 1 4 5 brfvopabrbr ⊢ F Trails ⁡ G P ↔ F Walks ⁡ G P ∧ Fun ⁡ F -1