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

Metamath Proof Explorer

Theorem isspth

Description: Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion isspth ⊢ F SPaths ⁡ G P ↔ F Trails ⁡ G P ∧ Fun ⁡ P -1

Proof

Step Hyp Ref Expression
1 spthsfval ⊢ SPaths ⁡ G = f p | f Trails ⁡ G p ∧ Fun ⁡ p -1
2 cnveq ⊢ p = P → p -1 = P -1
3 2 funeqd ⊢ p = P → Fun ⁡ p -1 ↔ Fun ⁡ P -1
4 3 adantl ⊢ f = F ∧ p = P → Fun ⁡ p -1 ↔ Fun ⁡ P -1
5 reltrls ⊢ Rel ⁡ Trails ⁡ G
6 1 4 5 brfvopabrbr ⊢ F SPaths ⁡ G P ↔ F Trails ⁡ G P ∧ Fun ⁡ P -1