Metamath Proof Explorer

Theorem vtxduhgr0edgnel

Description: A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢V=Vtx⁡G
vtxdushgrfvedg.e ⊢E=Edg⁡G
vtxdushgrfvedg.d ⊢D=VtxDeg⁡G
Assertion vtxduhgr0edgnel ⊢G∈UHGraph∧U∈V→D⁡U=0↔¬∃e∈EU∈e

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢V=Vtx⁡G
2 vtxdushgrfvedg.e ⊢E=Edg⁡G
3 vtxdushgrfvedg.d ⊢D=VtxDeg⁡G
4 eqid ⊢iEdg⁡G=iEdg⁡G
5 1 4 3 vtxd0nedgb ⊢U∈V→D⁡U=0↔¬∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
6 5 adantl ⊢G∈UHGraph∧U∈V→D⁡U=0↔¬∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
7 4 2 uhgrvtxedgiedgb ⊢G∈UHGraph∧U∈V→∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i↔∃e∈EU∈e
8 7 notbid ⊢G∈UHGraph∧U∈V→¬∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i↔¬∃e∈EU∈e
9 6 8 bitrd ⊢G∈UHGraph∧U∈V→D⁡U=0↔¬∃e∈EU∈e