Metamath Proof Explorer

Theorem uhgrnbgr0nb

Description: A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Assertion uhgrnbgr0nb 
|- ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) -> ( G NeighbVtx N ) = (/) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 nbuhgr 
 |-  ( ( G e. UHGraph /\ N e. _V ) -> ( G NeighbVtx N ) = { n e. ( ( Vtx ` G ) \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } )
4 3 adantlr 
 |-  ( ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) /\ N e. _V ) -> ( G NeighbVtx N ) = { n e. ( ( Vtx ` G ) \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } )
5 df-nel 
 |-  ( N e/ e <-> -. N e. e )
6 prssg 
 |-  ( ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
7 simpl 
 |-  ( ( N e. e /\ n e. e ) -> N e. e )
8 6 7 syl6bir 
 |-  ( ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) -> ( { N , n } C_ e -> N e. e ) )
9 8 ad2antlr 
 |-  ( ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) /\ e e. ( Edg ` G ) ) -> ( { N , n } C_ e -> N e. e ) )
10 9 con3d 
 |-  ( ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) /\ e e. ( Edg ` G ) ) -> ( -. N e. e -> -. { N , n } C_ e ) )
11 5 10 syl5bi 
 |-  ( ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) /\ e e. ( Edg ` G ) ) -> ( N e/ e -> -. { N , n } C_ e ) )
12 11 ralimdva 
 |-  ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) -> ( A. e e. ( Edg ` G ) N e/ e -> A. e e. ( Edg ` G ) -. { N , n } C_ e ) )
13 12 imp 
 |-  ( ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) /\ A. e e. ( Edg ` G ) N e/ e ) -> A. e e. ( Edg ` G ) -. { N , n } C_ e )
14 ralnex 
 |-  ( A. e e. ( Edg ` G ) -. { N , n } C_ e <-> -. E. e e. ( Edg ` G ) { N , n } C_ e )
15 13 14 sylib 
 |-  ( ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) /\ A. e e. ( Edg ` G ) N e/ e ) -> -. E. e e. ( Edg ` G ) { N , n } C_ e )
16 15 expcom 
 |-  ( A. e e. ( Edg ` G ) N e/ e -> ( ( G e. UHGraph /\ ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) ) -> -. E. e e. ( Edg ` G ) { N , n } C_ e ) )
17 16 expd 
 |-  ( A. e e. ( Edg ` G ) N e/ e -> ( G e. UHGraph -> ( ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) -> -. E. e e. ( Edg ` G ) { N , n } C_ e ) ) )
18 17 impcom 
 |-  ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) -> ( ( N e. _V /\ n e. ( ( Vtx ` G ) \ { N } ) ) -> -. E. e e. ( Edg ` G ) { N , n } C_ e ) )
19 18 expdimp 
 |-  ( ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) /\ N e. _V ) -> ( n e. ( ( Vtx ` G ) \ { N } ) -> -. E. e e. ( Edg ` G ) { N , n } C_ e ) )
20 19 ralrimiv 
 |-  ( ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) /\ N e. _V ) -> A. n e. ( ( Vtx ` G ) \ { N } ) -. E. e e. ( Edg ` G ) { N , n } C_ e )
21 rabeq0 
 |-  ( { n e. ( ( Vtx ` G ) \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } = (/) <-> A. n e. ( ( Vtx ` G ) \ { N } ) -. E. e e. ( Edg ` G ) { N , n } C_ e )
22 20 21 sylibr 
 |-  ( ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) /\ N e. _V ) -> { n e. ( ( Vtx ` G ) \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } = (/) )
23 4 22 eqtrd 
 |-  ( ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) /\ N e. _V ) -> ( G NeighbVtx N ) = (/) )
24 23 expcom 
 |-  ( N e. _V -> ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) -> ( G NeighbVtx N ) = (/) ) )
25 id 
 |-  ( -. N e. _V -> -. N e. _V )
26 25 intnand 
 |-  ( -. N e. _V -> -. ( G e. _V /\ N e. _V ) )
27 nbgrprc0 
 |-  ( -. ( G e. _V /\ N e. _V ) -> ( G NeighbVtx N ) = (/) )
28 26 27 syl 
 |-  ( -. N e. _V -> ( G NeighbVtx N ) = (/) )
29 28 a1d 
 |-  ( -. N e. _V -> ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) -> ( G NeighbVtx N ) = (/) ) )
30 24 29 pm2.61i 
 |-  ( ( G e. UHGraph /\ A. e e. ( Edg ` G ) N e/ e ) -> ( G NeighbVtx N ) = (/) )