Metamath Proof Explorer

Theorem usgrop

Description: A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020) (Proof shortened by AV, 30-Nov-2020)

Ref Expression
Assertion usgrop ⊢G∈USGraph→Vtx⁡GiEdg⁡G∈USGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 1 2 usgrfs ⊢G∈USGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G|x=2
4 fvex ⊢Vtx⁡G∈V
5 fvex ⊢iEdg⁡G∈V
6 4 5 pm3.2i ⊢Vtx⁡G∈V∧iEdg⁡G∈V
7 isusgrop ⊢Vtx⁡G∈V∧iEdg⁡G∈V→Vtx⁡GiEdg⁡G∈USGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G|x=2
8 6 7 mp1i ⊢G∈USGraph→Vtx⁡GiEdg⁡G∈USGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G|x=2
9 3 8 mpbird ⊢G∈USGraph→Vtx⁡GiEdg⁡G∈USGraph