Theorem upgrspthswlk

Description: The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p_0, p_1, p_2 } be a hyperedge, then ( p_0, e, p_1, e, p_2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021) (Proof shortened by AV, 17-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	upgrspthswlk	|- ( G e. UPGraph -> ( SPaths ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )

Proof

Step	Hyp	Ref	Expression
1		spthsfval	|- ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }
2		istrl	|- ( f ( Trails ` G ) p <-> ( f ( Walks ` G ) p /\ Fun `' f ) )
3		upgrwlkdvde	|- ( ( G e. UPGraph /\ f ( Walks ` G ) p /\ Fun `' p ) -> Fun `' f )
4	3	3exp	|- ( G e. UPGraph -> ( f ( Walks ` G ) p -> ( Fun `' p -> Fun `' f ) ) )
5	4	com23	|- ( G e. UPGraph -> ( Fun `' p -> ( f ( Walks ` G ) p -> Fun `' f ) ) )
6	5	imp	|- ( ( G e. UPGraph /\ Fun `' p ) -> ( f ( Walks ` G ) p -> Fun `' f ) )
7	6	pm4.71d	|- ( ( G e. UPGraph /\ Fun `' p ) -> ( f ( Walks ` G ) p <-> ( f ( Walks ` G ) p /\ Fun `' f ) ) )
8	2 7	bitr4id	|- ( ( G e. UPGraph /\ Fun `' p ) -> ( f ( Trails ` G ) p <-> f ( Walks ` G ) p ) )
9	8	ex	|- ( G e. UPGraph -> ( Fun `' p -> ( f ( Trails ` G ) p <-> f ( Walks ` G ) p ) ) )
10	9	pm5.32rd	|- ( G e. UPGraph -> ( ( f ( Trails ` G ) p /\ Fun `' p ) <-> ( f ( Walks ` G ) p /\ Fun `' p ) ) )
11	10	opabbidv	|- ( G e. UPGraph -> { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) } = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )
12	1 11	syl5eq	|- ( G e. UPGraph -> ( SPaths ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )