Metamath Proof Explorer

Theorem vtxduhgr0e

Description: The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e . (Contributed by AV, 15-Dec-2020)

Ref Expression
Hypotheses vtxduhgr0e.v ⊢ V = Vtx ⁡ G
vtxduhgr0e.e ⊢ E = Edg ⁡ G
Assertion vtxduhgr0e ⊢ G ∈ UHGraph ∧ U ∈ V ∧ E = ∅ → VtxDeg ⁡ G ⁡ U = 0

Proof

Step Hyp Ref Expression
1 vtxduhgr0e.v ⊢ V = Vtx ⁡ G
2 vtxduhgr0e.e ⊢ E = Edg ⁡ G
3 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
4 3 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
5 3 2 edg0iedg0 ⊢ Fun ⁡ iEdg ⁡ G → E = ∅ ↔ iEdg ⁡ G = ∅
6 4 5 syl ⊢ G ∈ UHGraph → E = ∅ ↔ iEdg ⁡ G = ∅
7 6 adantr ⊢ G ∈ UHGraph ∧ U ∈ V → E = ∅ ↔ iEdg ⁡ G = ∅
8 1 3 vtxdg0e ⊢ U ∈ V ∧ iEdg ⁡ G = ∅ → VtxDeg ⁡ G ⁡ U = 0
9 8 ex ⊢ U ∈ V → iEdg ⁡ G = ∅ → VtxDeg ⁡ G ⁡ U = 0
10 9 adantl ⊢ G ∈ UHGraph ∧ U ∈ V → iEdg ⁡ G = ∅ → VtxDeg ⁡ G ⁡ U = 0
11 7 10 sylbid ⊢ G ∈ UHGraph ∧ U ∈ V → E = ∅ → VtxDeg ⁡ G ⁡ U = 0
12 11 3impia ⊢ G ∈ UHGraph ∧ U ∈ V ∧ E = ∅ → VtxDeg ⁡ G ⁡ U = 0