Metamath Proof Explorer

Theorem wspthsnonn0vne

Description: If the set of simple paths of length at least 1 between two vertices is not empty, the two vertices must be different. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 16-May-2021)

Ref Expression
Assertion wspthsnonn0vne 
|- ( ( N e. NN /\ ( X ( N WSPathsNOn G ) Y ) =/= (/) ) -> X =/= Y )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( ( X ( N WSPathsNOn G ) Y ) =/= (/) <-> E. p p e. ( X ( N WSPathsNOn G ) Y ) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 wspthnonp 
 |-  ( p e. ( X ( N WSPathsNOn G ) Y ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) /\ ( p e. ( X ( N WWalksNOn G ) Y ) /\ E. f f ( X ( SPathsOn ` G ) Y ) p ) ) )
4 wwlknon 
 |-  ( p e. ( X ( N WWalksNOn G ) Y ) <-> ( p e. ( N WWalksN G ) /\ ( p ` 0 ) = X /\ ( p ` N ) = Y ) )
5 iswwlksn 
 |-  ( N e. NN0 -> ( p e. ( N WWalksN G ) <-> ( p e. ( WWalks ` G ) /\ ( # ` p ) = ( N + 1 ) ) ) )
6 spthonisspth 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> f ( SPaths ` G ) p )
7 spthispth 
 |-  ( f ( SPaths ` G ) p -> f ( Paths ` G ) p )
8 pthiswlk 
 |-  ( f ( Paths ` G ) p -> f ( Walks ` G ) p )
9 wlklenvm1 
 |-  ( f ( Walks ` G ) p -> ( # ` f ) = ( ( # ` p ) - 1 ) )
10 6 7 8 9 4syl 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( # ` f ) = ( ( # ` p ) - 1 ) )
11 oveq1 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( ( # ` p ) - 1 ) = ( ( N + 1 ) - 1 ) )
12 11 eqeq2d 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( ( # ` f ) = ( ( # ` p ) - 1 ) <-> ( # ` f ) = ( ( N + 1 ) - 1 ) ) )
13 simpr 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( # ` f ) = ( ( N + 1 ) - 1 ) )
14 nncn 
 |-  ( N e. NN -> N e. CC )
15 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
16 14 15 syl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
17 16 adantr 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( ( N + 1 ) - 1 ) = N )
18 13 17 eqtrd 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( # ` f ) = N )
19 nnne0 
 |-  ( N e. NN -> N =/= 0 )
20 19 adantr 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> N =/= 0 )
21 18 20 eqnetrd 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( # ` f ) =/= 0 )
22 spthonepeq 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( X = Y <-> ( # ` f ) = 0 ) )
23 22 necon3bid 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( X =/= Y <-> ( # ` f ) =/= 0 ) )
24 21 23 syl5ibrcom 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( f ( X ( SPathsOn ` G ) Y ) p -> X =/= Y ) )
25 24 expcom 
 |-  ( ( # ` f ) = ( ( N + 1 ) - 1 ) -> ( N e. NN -> ( f ( X ( SPathsOn ` G ) Y ) p -> X =/= Y ) ) )
26 25 com23 
 |-  ( ( # ` f ) = ( ( N + 1 ) - 1 ) -> ( f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) )
27 12 26 biimtrdi 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( ( # ` f ) = ( ( # ` p ) - 1 ) -> ( f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
28 27 com13 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( ( # ` f ) = ( ( # ` p ) - 1 ) -> ( ( # ` p ) = ( N + 1 ) -> ( N e. NN -> X =/= Y ) ) ) )
29 10 28 mpd 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( ( # ` p ) = ( N + 1 ) -> ( N e. NN -> X =/= Y ) ) )
30 29 exlimiv 
 |-  ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( ( # ` p ) = ( N + 1 ) -> ( N e. NN -> X =/= Y ) ) )
31 30 com12 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) )
32 31 adantl 
 |-  ( ( p e. ( WWalks ` G ) /\ ( # ` p ) = ( N + 1 ) ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) )
33 5 32 biimtrdi 
 |-  ( N e. NN0 -> ( p e. ( N WWalksN G ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
34 33 adantr 
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( p e. ( N WWalksN G ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
35 34 adantr 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) ) -> ( p e. ( N WWalksN G ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
36 35 com12 
 |-  ( p e. ( N WWalksN G ) -> ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
37 36 3ad2ant1 
 |-  ( ( p e. ( N WWalksN G ) /\ ( p ` 0 ) = X /\ ( p ` N ) = Y ) -> ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
38 37 com12 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) ) -> ( ( p e. ( N WWalksN G ) /\ ( p ` 0 ) = X /\ ( p ` N ) = Y ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
39 4 38 biimtrid 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) ) -> ( p e. ( X ( N WWalksNOn G ) Y ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
40 39 impd 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) ) -> ( ( p e. ( X ( N WWalksNOn G ) Y ) /\ E. f f ( X ( SPathsOn ` G ) Y ) p ) -> ( N e. NN -> X =/= Y ) ) )
41 40 3impia 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( X e. ( Vtx ` G ) /\ Y e. ( Vtx ` G ) ) /\ ( p e. ( X ( N WWalksNOn G ) Y ) /\ E. f f ( X ( SPathsOn ` G ) Y ) p ) ) -> ( N e. NN -> X =/= Y ) )
42 3 41 syl 
 |-  ( p e. ( X ( N WSPathsNOn G ) Y ) -> ( N e. NN -> X =/= Y ) )
43 42 exlimiv 
 |-  ( E. p p e. ( X ( N WSPathsNOn G ) Y ) -> ( N e. NN -> X =/= Y ) )
44 1 43 sylbi 
 |-  ( ( X ( N WSPathsNOn G ) Y ) =/= (/) -> ( N e. NN -> X =/= Y ) )
45 44 impcom 
 |-  ( ( N e. NN /\ ( X ( N WSPathsNOn G ) Y ) =/= (/) ) -> X =/= Y )