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

Metamath Proof Explorer

Theorem usgredgss

Description: The set of edges of a simple graph is a subset of the set of proper unordered pairs of vertices. (Contributed by AV, 1-Jan-2020) (Revised by AV, 14-Oct-2020)

Ref Expression
Assertion usgredgss ⊢ G ∈ USGraph → 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 usgrfs ⊢ G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2
5 f1f ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | x = 2
6 frn ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | x = 2 → ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G | x = 2
7 4 5 6 3syl ⊢ G ∈ USGraph → ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G | x = 2
8 1 7 eqsstrid ⊢ G ∈ USGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G | x = 2