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 8 9 syl 
 |-  ( f ( Paths ` G ) p -> ( # ` f ) = ( ( # ` p ) - 1 ) )
11 6 7 10 3syl 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( # ` f ) = ( ( # ` p ) - 1 ) )
12 oveq1 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( ( # ` p ) - 1 ) = ( ( N + 1 ) - 1 ) )
13 12 eqeq2d 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( ( # ` f ) = ( ( # ` p ) - 1 ) <-> ( # ` f ) = ( ( N + 1 ) - 1 ) ) )
14 simpr 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( # ` f ) = ( ( N + 1 ) - 1 ) )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
17 15 16 syl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
18 17 adantr 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( ( N + 1 ) - 1 ) = N )
19 14 18 eqtrd 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( # ` f ) = N )
20 nnne0 
 |-  ( N e. NN -> N =/= 0 )
21 20 adantr 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> N =/= 0 )
22 19 21 eqnetrd 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( # ` f ) =/= 0 )
23 spthonepeq 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( X = Y <-> ( # ` f ) = 0 ) )
24 23 necon3bid 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( X =/= Y <-> ( # ` f ) =/= 0 ) )
25 22 24 syl5ibrcom 
 |-  ( ( N e. NN /\ ( # ` f ) = ( ( N + 1 ) - 1 ) ) -> ( f ( X ( SPathsOn ` G ) Y ) p -> X =/= Y ) )
26 25 expcom 
 |-  ( ( # ` f ) = ( ( N + 1 ) - 1 ) -> ( N e. NN -> ( f ( X ( SPathsOn ` G ) Y ) p -> X =/= Y ) ) )
27 26 com23 
 |-  ( ( # ` f ) = ( ( N + 1 ) - 1 ) -> ( f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) )
28 13 27 biimtrdi 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( ( # ` f ) = ( ( # ` p ) - 1 ) -> ( f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
29 28 com13 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( ( # ` f ) = ( ( # ` p ) - 1 ) -> ( ( # ` p ) = ( N + 1 ) -> ( N e. NN -> X =/= Y ) ) ) )
30 11 29 mpd 
 |-  ( f ( X ( SPathsOn ` G ) Y ) p -> ( ( # ` p ) = ( N + 1 ) -> ( N e. NN -> X =/= Y ) ) )
31 30 exlimiv 
 |-  ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( ( # ` p ) = ( N + 1 ) -> ( N e. NN -> X =/= Y ) ) )
32 31 com12 
 |-  ( ( # ` p ) = ( N + 1 ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) )
33 32 adantl 
 |-  ( ( p e. ( WWalks ` G ) /\ ( # ` p ) = ( N + 1 ) ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) )
34 5 33 biimtrdi 
 |-  ( N e. NN0 -> ( 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 ) -> ( p e. ( N WWalksN G ) -> ( E. f f ( X ( SPathsOn ` G ) Y ) p -> ( N e. NN -> X =/= Y ) ) ) )
36 35 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 ) ) ) )
37 36 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 ) ) ) )
38 37 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 ) ) ) )
39 38 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 ) ) ) )
40 4 39 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 ) ) ) )
41 40 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 ) ) )
42 41 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 ) )
43 3 42 syl 
 |-  ( p e. ( X ( N WSPathsNOn G ) Y ) -> ( N e. NN -> X =/= Y ) )
44 43 exlimiv 
 |-  ( E. p p e. ( X ( N WSPathsNOn G ) Y ) -> ( N e. NN -> X =/= Y ) )
45 1 44 sylbi 
 |-  ( ( X ( N WSPathsNOn G ) Y ) =/= (/) -> ( N e. NN -> X =/= Y ) )
46 45 impcom 
 |-  ( ( N e. NN /\ ( X ( N WSPathsNOn G ) Y ) =/= (/) ) -> X =/= Y )