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 ⁡ G iEdg ⁡ 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-1 x ∈ 𝒫 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 ⁡ G iEdg ⁡ G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2
8 6 7 mp1i ⊢ G ∈ USGraph → Vtx ⁡ G iEdg ⁡ G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2
9 3 8 mpbird ⊢ G ∈ USGraph → Vtx ⁡ G iEdg ⁡ G ∈ USGraph