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 ∖ ∅