Metamath Proof Explorer

Theorem cusgrop

Description: A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020)

Ref Expression
Assertion cusgrop ⊢ G ∈ ComplUSGraph → Vtx ⁡ G iEdg ⁡ G ∈ ComplUSGraph

Proof

Step Hyp Ref Expression
1 usgrop ⊢ G ∈ USGraph → Vtx ⁡ G iEdg ⁡ G ∈ USGraph
2 cplgrop ⊢ G ∈ ComplGraph → Vtx ⁡ G iEdg ⁡ G ∈ ComplGraph
3 1 2 anim12i ⊢ G ∈ USGraph ∧ G ∈ ComplGraph → Vtx ⁡ G iEdg ⁡ G ∈ USGraph ∧ Vtx ⁡ G iEdg ⁡ G ∈ ComplGraph
4 iscusgr ⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ G ∈ ComplGraph
5 iscusgr ⊢ Vtx ⁡ G iEdg ⁡ G ∈ ComplUSGraph ↔ Vtx ⁡ G iEdg ⁡ G ∈ USGraph ∧ Vtx ⁡ G iEdg ⁡ G ∈ ComplGraph
6 3 4 5 3imtr4i ⊢ G ∈ ComplUSGraph → Vtx ⁡ G iEdg ⁡ G ∈ ComplUSGraph