This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nbumgr

Description: The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v 
|- V = ( Vtx ` G )
nbuhgr.e 
|- E = ( Edg ` G )
Assertion nbumgr 
|- ( G e. UMGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )

Proof

Step Hyp Ref Expression
1 nbuhgr.v 
 |-  V = ( Vtx ` G )
2 nbuhgr.e 
 |-  E = ( Edg ` G )
3 1 2 nbumgrvtx 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
4 3 expcom 
 |-  ( N e. V -> ( G e. UMGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } ) )
5 df-nel 
 |-  ( N e/ V <-> -. N e. V )
6 1 nbgrnvtx0 
 |-  ( N e/ V -> ( G NeighbVtx N ) = (/) )
7 5 6 sylbir 
 |-  ( -. N e. V -> ( G NeighbVtx N ) = (/) )
8 7 adantr 
 |-  ( ( -. N e. V /\ G e. UMGraph ) -> ( G NeighbVtx N ) = (/) )
9 1 2 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { N , n } e. E ) -> ( N e. V /\ n e. V ) )
10 9 simpld 
 |-  ( ( G e. UMGraph /\ { N , n } e. E ) -> N e. V )
11 10 ex 
 |-  ( G e. UMGraph -> ( { N , n } e. E -> N e. V ) )
12 11 adantl 
 |-  ( ( n e. V /\ G e. UMGraph ) -> ( { N , n } e. E -> N e. V ) )
13 12 con3d 
 |-  ( ( n e. V /\ G e. UMGraph ) -> ( -. N e. V -> -. { N , n } e. E ) )
14 13 ex 
 |-  ( n e. V -> ( G e. UMGraph -> ( -. N e. V -> -. { N , n } e. E ) ) )
15 14 com13 
 |-  ( -. N e. V -> ( G e. UMGraph -> ( n e. V -> -. { N , n } e. E ) ) )
16 15 imp 
 |-  ( ( -. N e. V /\ G e. UMGraph ) -> ( n e. V -> -. { N , n } e. E ) )
17 16 ralrimiv 
 |-  ( ( -. N e. V /\ G e. UMGraph ) -> A. n e. V -. { N , n } e. E )
18 rabeq0 
 |-  ( { n e. V | { N , n } e. E } = (/) <-> A. n e. V -. { N , n } e. E )
19 17 18 sylibr 
 |-  ( ( -. N e. V /\ G e. UMGraph ) -> { n e. V | { N , n } e. E } = (/) )
20 8 19 eqtr4d 
 |-  ( ( -. N e. V /\ G e. UMGraph ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
21 20 ex 
 |-  ( -. N e. V -> ( G e. UMGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } ) )
22 4 21 pm2.61i 
 |-  ( G e. UMGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )