Metamath Proof Explorer

Theorem upgruhgr

Description: An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 10-Oct-2020)

Ref Expression
Assertion upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 upgrf ⊢ G ∈ UPGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
4 ssrab2 ⊢ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ⊆ 𝒫 Vtx ⁡ G ∖ ∅
5 fss ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ∧ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ⊆ 𝒫 Vtx ⁡ G ∖ ∅ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
6 3 4 5 sylancl ⊢ G ∈ UPGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
7 1 2 isuhgr ⊢ G ∈ UPGraph → G ∈ UHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
8 6 7 mpbird ⊢ G ∈ UPGraph → G ∈ UHGraph