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 | ⊢ ( 𝐺 ∈ UPGraph → ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | edgval | ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) | |
2 | eqid | ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) | |
3 | eqid | ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) | |
4 | 2 3 | upgrf | ⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
5 | 4 | frnd | ⊢ ( 𝐺 ∈ UPGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
6 | 1 5 | eqsstrid | ⊢ ( 𝐺 ∈ UPGraph → ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |