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 ∈ E U ∈ 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 ⁡ G U ∈ iEdg ⁡ G ⁡ i
6 5 adantl ⊢ G ∈ UHGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i
7 4 2 uhgrvtxedgiedgb ⊢ G ∈ UHGraph ∧ U ∈ V → ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i ↔ ∃ e ∈ E U ∈ e
8 7 notbid ⊢ G ∈ UHGraph ∧ U ∈ V → ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i ↔ ¬ ∃ e ∈ E U ∈ e
9 6 8 bitrd ⊢ G ∈ UHGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ e ∈ E U ∈ e