Metamath Proof Explorer


Theorem vtxdlfuhgr1v

Description: The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021)

Ref Expression
Hypotheses vtxdlfuhgr1v.v V=VtxG
vtxdlfuhgr1v.i I=iEdgG
vtxdlfuhgr1v.e E=x𝒫V|2x
Assertion vtxdlfuhgr1v GUHGraphV=1I:domIEUVVtxDegGU=0

Proof

Step Hyp Ref Expression
1 vtxdlfuhgr1v.v V=VtxG
2 vtxdlfuhgr1v.i I=iEdgG
3 vtxdlfuhgr1v.e E=x𝒫V|2x
4 simpl1 GUHGraphV=1I:domIEUVGUHGraph
5 simpr GUHGraphV=1I:domIEUVUV
6 1 2 3 lfuhgr1v0e GUHGraphV=1I:domIEEdgG=
7 6 adantr GUHGraphV=1I:domIEUVEdgG=
8 eqid EdgG=EdgG
9 1 8 vtxduhgr0e GUHGraphUVEdgG=VtxDegGU=0
10 4 5 7 9 syl3anc GUHGraphV=1I:domIEUVVtxDegGU=0
11 10 ex GUHGraphV=1I:domIEUVVtxDegGU=0