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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nbuhgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	nbumgr	⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )

Proof

Step	Hyp	Ref	Expression
1		nbuhgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbuhgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	nbumgrvtx	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
4	3	expcom	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
5		df-nel	⊢ ( 𝑁 ∉ 𝑉 ↔ ¬ 𝑁 ∈ 𝑉 )
6	1	nbgrnvtx0	⊢ ( 𝑁 ∉ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
7	5 6	sylbir	⊢ ( ¬ 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
8	7	adantr	⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
9	1 2	umgrpredgv	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
10	9	simpld	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → 𝑁 ∈ 𝑉 )
11	10	ex	⊢ ( 𝐺 ∈ UMGraph → ( { 𝑁 , 𝑛 } ∈ 𝐸 → 𝑁 ∈ 𝑉 ) )
12	11	adantl	⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( { 𝑁 , 𝑛 } ∈ 𝐸 → 𝑁 ∈ 𝑉 ) )
13	12	con3d	⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( ¬ 𝑁 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) )
14	13	ex	⊢ ( 𝑛 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( ¬ 𝑁 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) ) )
15	14	com13	⊢ ( ¬ 𝑁 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( 𝑛 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) ) )
16	15	imp	⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( 𝑛 ∈ 𝑉 → ¬ { 𝑁 , 𝑛 } ∈ 𝐸 ) )
17	16	ralrimiv	⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ∀ 𝑛 ∈ 𝑉 ¬ { 𝑁 , 𝑛 } ∈ 𝐸 )
18		rabeq0	⊢ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } = ∅ ↔ ∀ 𝑛 ∈ 𝑉 ¬ { 𝑁 , 𝑛 } ∈ 𝐸 )
19	17 18	sylibr	⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } = ∅ )
20	8 19	eqtr4d	⊢ ( ( ¬ 𝑁 ∈ 𝑉 ∧ 𝐺 ∈ UMGraph ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
21	20	ex	⊢ ( ¬ 𝑁 ∈ 𝑉 → ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
22	4 21	pm2.61i	⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )