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-1x∈𝒫Vtx⁡G∖∅|x≤2
11 6 9 10 syl2anr ⊢G∈UPGraph∧G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
12 4 5 isuspgr ⊢G∈UPGraph→G∈USHGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
13 12 adantr ⊢G∈UPGraph∧G∈USHGraph→G∈USHGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
14 11 13 mpbird ⊢G∈UPGraph∧G∈USHGraph→G∈USHGraph
15 3 14 impbii ⊢G∈USHGraph↔G∈UPGraph∧G∈USHGraph