Metamath Proof Explorer

Theorem uhgredgn0

Description: An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020)

Ref Expression
Assertion uhgredgn0 ⊢G∈UHGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G∖∅

Proof

Step Hyp Ref Expression
1 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
2 eqid ⊢Vtx⁡G=Vtx⁡G
3 eqid ⊢iEdg⁡G=iEdg⁡G
4 2 3 uhgrf ⊢G∈UHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫Vtx⁡G∖∅
5 4 frnd ⊢G∈UHGraph→ran⁡iEdg⁡G⊆𝒫Vtx⁡G∖∅
6 1 5 eqsstrid ⊢G∈UHGraph→Edg⁡G⊆𝒫Vtx⁡G∖∅
7 6 sselda ⊢G∈UHGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G∖∅