This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgredgss

Description: The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 29-Nov-2020)

Ref Expression
Assertion upgredgss ⊢ G ∈ UPGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2

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 upgrf ⊢ G ∈ UPGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
5 4 frnd ⊢ G ∈ UPGraph → ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
6 1 5 eqsstrid ⊢ G ∈ UPGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2