Metamath Proof Explorer

Theorem wspthneq1eq2

Description: Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021)

Ref Expression
Assertion wspthneq1eq2 
|- ( ( P e. ( A ( N WSPathsNOn G ) B ) /\ P e. ( C ( N WSPathsNOn G ) D ) ) -> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wspthnonp 
 |-  ( P e. ( A ( N WSPathsNOn G ) B ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( P e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) P ) ) )
3 1 wspthnonp 
 |-  ( P e. ( C ( N WSPathsNOn G ) D ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( P e. ( C ( N WWalksNOn G ) D ) /\ E. h h ( C ( SPathsOn ` G ) D ) P ) ) )
4 simp3r 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( P e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) P ) ) -> E. f f ( A ( SPathsOn ` G ) B ) P )
5 simp3r 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( P e. ( C ( N WWalksNOn G ) D ) /\ E. h h ( C ( SPathsOn ` G ) D ) P ) ) -> E. h h ( C ( SPathsOn ` G ) D ) P )
6 spthonpthon 
 |-  ( f ( A ( SPathsOn ` G ) B ) P -> f ( A ( PathsOn ` G ) B ) P )
7 spthonpthon 
 |-  ( h ( C ( SPathsOn ` G ) D ) P -> h ( C ( PathsOn ` G ) D ) P )
8 6 7 anim12i 
 |-  ( ( f ( A ( SPathsOn ` G ) B ) P /\ h ( C ( SPathsOn ` G ) D ) P ) -> ( f ( A ( PathsOn ` G ) B ) P /\ h ( C ( PathsOn ` G ) D ) P ) )
9 pthontrlon 
 |-  ( f ( A ( PathsOn ` G ) B ) P -> f ( A ( TrailsOn ` G ) B ) P )
10 pthontrlon 
 |-  ( h ( C ( PathsOn ` G ) D ) P -> h ( C ( TrailsOn ` G ) D ) P )
11 trlsonwlkon 
 |-  ( f ( A ( TrailsOn ` G ) B ) P -> f ( A ( WalksOn ` G ) B ) P )
12 trlsonwlkon 
 |-  ( h ( C ( TrailsOn ` G ) D ) P -> h ( C ( WalksOn ` G ) D ) P )
13 11 12 anim12i 
 |-  ( ( f ( A ( TrailsOn ` G ) B ) P /\ h ( C ( TrailsOn ` G ) D ) P ) -> ( f ( A ( WalksOn ` G ) B ) P /\ h ( C ( WalksOn ` G ) D ) P ) )
14 9 10 13 syl2an 
 |-  ( ( f ( A ( PathsOn ` G ) B ) P /\ h ( C ( PathsOn ` G ) D ) P ) -> ( f ( A ( WalksOn ` G ) B ) P /\ h ( C ( WalksOn ` G ) D ) P ) )
15 wlksoneq1eq2 
 |-  ( ( f ( A ( WalksOn ` G ) B ) P /\ h ( C ( WalksOn ` G ) D ) P ) -> ( A = C /\ B = D ) )
16 8 14 15 3syl 
 |-  ( ( f ( A ( SPathsOn ` G ) B ) P /\ h ( C ( SPathsOn ` G ) D ) P ) -> ( A = C /\ B = D ) )
17 16 expcom 
 |-  ( h ( C ( SPathsOn ` G ) D ) P -> ( f ( A ( SPathsOn ` G ) B ) P -> ( A = C /\ B = D ) ) )
18 17 exlimiv 
 |-  ( E. h h ( C ( SPathsOn ` G ) D ) P -> ( f ( A ( SPathsOn ` G ) B ) P -> ( A = C /\ B = D ) ) )
19 18 com12 
 |-  ( f ( A ( SPathsOn ` G ) B ) P -> ( E. h h ( C ( SPathsOn ` G ) D ) P -> ( A = C /\ B = D ) ) )
20 19 exlimiv 
 |-  ( E. f f ( A ( SPathsOn ` G ) B ) P -> ( E. h h ( C ( SPathsOn ` G ) D ) P -> ( A = C /\ B = D ) ) )
21 20 imp 
 |-  ( ( E. f f ( A ( SPathsOn ` G ) B ) P /\ E. h h ( C ( SPathsOn ` G ) D ) P ) -> ( A = C /\ B = D ) )
22 4 5 21 syl2an 
 |-  ( ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( P e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) P ) ) /\ ( ( N e. NN0 /\ G e. _V ) /\ ( C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( P e. ( C ( N WWalksNOn G ) D ) /\ E. h h ( C ( SPathsOn ` G ) D ) P ) ) ) -> ( A = C /\ B = D ) )
23 2 3 22 syl2an 
 |-  ( ( P e. ( A ( N WSPathsNOn G ) B ) /\ P e. ( C ( N WSPathsNOn G ) D ) ) -> ( A = C /\ B = D ) )