Metamath Proof Explorer


Theorem usgredgss

Description: The set of edges of a simple graph is a subset of the set of 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