Metamath Proof Explorer

Theorem uspgrupgrushgr

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

Ref Expression
Assertion uspgrupgrushgr ⊢ G ∈ USHGraph ↔ G ∈ UPGraph ∧ G ∈ USHGraph

Proof

Step Hyp Ref Expression
1 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
2 uspgrushgr ⊢ G ∈ USHGraph → G ∈ USHGraph
3 1 2 jca ⊢ G ∈ USHGraph → G ∈ UPGraph ∧ G ∈ USHGraph
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
6 4 5 ushgrf ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅
7 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
8 upgredgss ⊢ G ∈ UPGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
9 7 8 eqsstrrid ⊢ G ∈ UPGraph → ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
10 f1ssr ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅ ∧ ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
11 6 9 10 syl2anr ⊢ G ∈ UPGraph ∧ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
12 4 5 isuspgr ⊢ G ∈ UPGraph → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
13 12 adantr ⊢ G ∈ UPGraph ∧ G ∈ USHGraph → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
14 11 13 mpbird ⊢ G ∈ UPGraph ∧ G ∈ USHGraph → G ∈ USHGraph
15 3 14 impbii ⊢ G ∈ USHGraph ↔ G ∈ UPGraph ∧ G ∈ USHGraph