Metamath Proof Explorer

Theorem usgruspgr

Description: A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 isusgr ⊢ G ∈ USGraph → G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
4 2re ⊢ 2 ∈ ℝ
5 4 eqlei2 ⊢ x = 2 → x ≤ 2
6 5 a1i ⊢ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ → x = 2 → x ≤ 2
7 6 ss2rabi ⊢ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
8 f1ss ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 ∧ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
9 7 8 mpan2 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
10 3 9 biimtrdi ⊢ G ∈ USGraph → G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
11 1 2 isuspgr ⊢ G ∈ USGraph → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
12 10 11 sylibrd ⊢ G ∈ USGraph → G ∈ USGraph → G ∈ USHGraph
13 12 pm2.43i ⊢ G ∈ USGraph → G ∈ USHGraph