Metamath Proof Explorer

Theorem nbgr1vtx

Description: In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

Ref Expression
Assertion nbgr1vtx 
|- ( ( # ` ( Vtx ` G ) ) = 1 -> ( G NeighbVtx K ) = (/) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( Vtx ` G ) e. _V
2 hash1snb 
 |-  ( ( Vtx ` G ) e. _V -> ( ( # ` ( Vtx ` G ) ) = 1 <-> E. v ( Vtx ` G ) = { v } ) )
3 1 2 ax-mp 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 <-> E. v ( Vtx ` G ) = { v } )
4 ral0 
 |-  A. n e. (/) -. E. e e. ( Edg ` G ) { K , n } C_ e
5 eleq2 
 |-  ( ( Vtx ` G ) = { v } -> ( K e. ( Vtx ` G ) <-> K e. { v } ) )
6 simpr 
 |-  ( ( K = v /\ ( Vtx ` G ) = { v } ) -> ( Vtx ` G ) = { v } )
7 sneq 
 |-  ( K = v -> { K } = { v } )
8 7 adantr 
 |-  ( ( K = v /\ ( Vtx ` G ) = { v } ) -> { K } = { v } )
9 6 8 difeq12d 
 |-  ( ( K = v /\ ( Vtx ` G ) = { v } ) -> ( ( Vtx ` G ) \ { K } ) = ( { v } \ { v } ) )
10 difid 
 |-  ( { v } \ { v } ) = (/)
11 9 10 eqtrdi 
 |-  ( ( K = v /\ ( Vtx ` G ) = { v } ) -> ( ( Vtx ` G ) \ { K } ) = (/) )
12 11 ex 
 |-  ( K = v -> ( ( Vtx ` G ) = { v } -> ( ( Vtx ` G ) \ { K } ) = (/) ) )
13 elsni 
 |-  ( K e. { v } -> K = v )
14 12 13 syl11 
 |-  ( ( Vtx ` G ) = { v } -> ( K e. { v } -> ( ( Vtx ` G ) \ { K } ) = (/) ) )
15 5 14 sylbid 
 |-  ( ( Vtx ` G ) = { v } -> ( K e. ( Vtx ` G ) -> ( ( Vtx ` G ) \ { K } ) = (/) ) )
16 15 imp 
 |-  ( ( ( Vtx ` G ) = { v } /\ K e. ( Vtx ` G ) ) -> ( ( Vtx ` G ) \ { K } ) = (/) )
17 16 raleqdv 
 |-  ( ( ( Vtx ` G ) = { v } /\ K e. ( Vtx ` G ) ) -> ( A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e <-> A. n e. (/) -. E. e e. ( Edg ` G ) { K , n } C_ e ) )
18 4 17 mpbiri 
 |-  ( ( ( Vtx ` G ) = { v } /\ K e. ( Vtx ` G ) ) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
19 18 ex 
 |-  ( ( Vtx ` G ) = { v } -> ( K e. ( Vtx ` G ) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e ) )
20 19 exlimiv 
 |-  ( E. v ( Vtx ` G ) = { v } -> ( K e. ( Vtx ` G ) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e ) )
21 3 20 sylbi 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 -> ( K e. ( Vtx ` G ) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e ) )
22 21 impcom 
 |-  ( ( K e. ( Vtx ` G ) /\ ( # ` ( Vtx ` G ) ) = 1 ) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
23 22 nbgr0vtxlem 
 |-  ( ( K e. ( Vtx ` G ) /\ ( # ` ( Vtx ` G ) ) = 1 ) -> ( G NeighbVtx K ) = (/) )
24 23 ex 
 |-  ( K e. ( Vtx ` G ) -> ( ( # ` ( Vtx ` G ) ) = 1 -> ( G NeighbVtx K ) = (/) ) )
25 df-nel 
 |-  ( K e/ ( Vtx ` G ) <-> -. K e. ( Vtx ` G ) )
26 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
27 26 nbgrnvtx0 
 |-  ( K e/ ( Vtx ` G ) -> ( G NeighbVtx K ) = (/) )
28 25 27 sylbir 
 |-  ( -. K e. ( Vtx ` G ) -> ( G NeighbVtx K ) = (/) )
29 28 a1d 
 |-  ( -. K e. ( Vtx ` G ) -> ( ( # ` ( Vtx ` G ) ) = 1 -> ( G NeighbVtx K ) = (/) ) )
30 24 29 pm2.61i 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 -> ( G NeighbVtx K ) = (/) )