Metamath Proof Explorer

Theorem uhgredgrnv

Description: An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Assertion uhgredgrnv ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G ∧ N ∈ E → N ∈ Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 edguhgr ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G → E ∈ 𝒫 Vtx ⁡ G
2 elelpwi ⊢ N ∈ E ∧ E ∈ 𝒫 Vtx ⁡ G → N ∈ Vtx ⁡ G
3 2 expcom ⊢ E ∈ 𝒫 Vtx ⁡ G → N ∈ E → N ∈ Vtx ⁡ G
4 1 3 syl ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G → N ∈ E → N ∈ Vtx ⁡ G
5 4 3impia ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G ∧ N ∈ E → N ∈ Vtx ⁡ G