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 )