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→GNeighbVtxN=n∈V|Nn∈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→GNeighbVtxN=n∈V|Nn∈E
4 3 expcom ⊢N∈V→G∈UMGraph→GNeighbVtxN=n∈V|Nn∈E
5 df-nel ⊢N∉V↔¬N∈V
6 1 nbgrnvtx0 ⊢N∉V→GNeighbVtxN=∅
7 5 6 sylbir ⊢¬N∈V→GNeighbVtxN=∅
8 7 adantr ⊢¬N∈V∧G∈UMGraph→GNeighbVtxN=∅
9 1 2 umgrpredgv ⊢G∈UMGraph∧Nn∈E→N∈V∧n∈V
10 9 simpld ⊢G∈UMGraph∧Nn∈E→N∈V
11 10 ex ⊢G∈UMGraph→Nn∈E→N∈V
12 11 adantl ⊢n∈V∧G∈UMGraph→Nn∈E→N∈V
13 12 con3d ⊢n∈V∧G∈UMGraph→¬N∈V→¬Nn∈E
14 13 ex ⊢n∈V→G∈UMGraph→¬N∈V→¬Nn∈E
15 14 com13 ⊢¬N∈V→G∈UMGraph→n∈V→¬Nn∈E
16 15 imp ⊢¬N∈V∧G∈UMGraph→n∈V→¬Nn∈E
17 16 ralrimiv ⊢¬N∈V∧G∈UMGraph→∀n∈V¬Nn∈E
18 rabeq0 ⊢n∈V|Nn∈E=∅↔∀n∈V¬Nn∈E
19 17 18 sylibr ⊢¬N∈V∧G∈UMGraph→n∈V|Nn∈E=∅
20 8 19 eqtr4d ⊢¬N∈V∧G∈UMGraph→GNeighbVtxN=n∈V|Nn∈E
21 20 ex ⊢¬N∈V→G∈UMGraph→GNeighbVtxN=n∈V|Nn∈E
22 4 21 pm2.61i ⊢G∈UMGraph→GNeighbVtxN=n∈V|Nn∈E