Metamath Proof Explorer

Theorem usgrumgruspgr

Description: A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020)

Ref Expression
Assertion usgrumgruspgr ⊢ G ∈ USGraph ↔ G ∈ UMGraph ∧ G ∈ USHGraph

Proof

Step Hyp Ref Expression
1 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
2 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
3 1 2 jca ⊢ G ∈ USGraph → G ∈ UMGraph ∧ G ∈ USHGraph
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
6 4 5 uspgrf ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
7 umgredgss ⊢ G ∈ UMGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G | x = 2
8 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
9 prprrab ⊢ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 = x ∈ 𝒫 Vtx ⁡ G | x = 2
10 9 eqcomi ⊢ x ∈ 𝒫 Vtx ⁡ G | x = 2 = x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
11 7 8 10 3sstr3g ⊢ G ∈ UMGraph → ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
12 f1ssr ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ∧ ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
13 6 11 12 syl2anr ⊢ G ∈ UMGraph ∧ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
14 4 5 isusgr ⊢ G ∈ UMGraph → G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
15 14 adantr ⊢ G ∈ UMGraph ∧ G ∈ USHGraph → G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
16 13 15 mpbird ⊢ G ∈ UMGraph ∧ G ∈ USHGraph → G ∈ USGraph
17 3 16 impbii ⊢ G ∈ USGraph ↔ G ∈ UMGraph ∧ G ∈ USHGraph