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