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 ∈ UMGraph → G NeighbVtx N = n ∈ V | N n ∈ E

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ V = Vtx ⁡ G
2 nbuhgr.e ⊢ E = Edg ⁡ G
3 1 2 nbumgrvtx ⊢ G ∈ UMGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V | N n ∈ E
4 3 expcom ⊢ N ∈ V → G ∈ UMGraph → G NeighbVtx N = n ∈ V | N n ∈ E
5 df-nel ⊢ N ∉ V ↔ ¬ N ∈ V
6 1 nbgrnvtx0 ⊢ N ∉ V → G NeighbVtx N = ∅
7 5 6 sylbir ⊢ ¬ N ∈ V → G NeighbVtx N = ∅
8 7 adantr ⊢ ¬ N ∈ V ∧ G ∈ UMGraph → G NeighbVtx N = ∅
9 1 2 umgrpredgv ⊢ G ∈ UMGraph ∧ N n ∈ E → N ∈ V ∧ n ∈ V
10 9 simpld ⊢ G ∈ UMGraph ∧ N n ∈ E → N ∈ V
11 10 ex ⊢ G ∈ UMGraph → N n ∈ E → N ∈ V
12 11 adantl ⊢ n ∈ V ∧ G ∈ UMGraph → N n ∈ E → N ∈ V
13 12 con3d ⊢ n ∈ V ∧ G ∈ UMGraph → ¬ N ∈ V → ¬ N n ∈ E
14 13 ex ⊢ n ∈ V → G ∈ UMGraph → ¬ N ∈ V → ¬ N n ∈ E
15 14 com13 ⊢ ¬ N ∈ V → G ∈ UMGraph → n ∈ V → ¬ N n ∈ E
16 15 imp ⊢ ¬ N ∈ V ∧ G ∈ UMGraph → n ∈ V → ¬ N n ∈ E
17 16 ralrimiv ⊢ ¬ N ∈ V ∧ G ∈ UMGraph → ∀ n ∈ V ¬ N n ∈ E
18 rabeq0 ⊢ n ∈ V | N n ∈ E = ∅ ↔ ∀ n ∈ V ¬ N n ∈ E
19 17 18 sylibr ⊢ ¬ N ∈ V ∧ G ∈ UMGraph → n ∈ V | N n ∈ E = ∅
20 8 19 eqtr4d ⊢ ¬ N ∈ V ∧ G ∈ UMGraph → G NeighbVtx N = n ∈ V | N n ∈ E
21 20 ex ⊢ ¬ N ∈ V → G ∈ UMGraph → G NeighbVtx N = n ∈ V | N n ∈ E
22 4 21 pm2.61i ⊢ G ∈ UMGraph → G NeighbVtx N = n ∈ V | N n ∈ E