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 } )