This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐺 ∈ ComplUSGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplUSGraph )

Proof

Step Hyp Ref Expression
1 usgrop ⊢ ( 𝐺 ∈ USGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph )
2 cplgrop ⊢ ( 𝐺 ∈ ComplGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplGraph )
3 1 2 anim12i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph ∧ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplGraph ) )
4 iscusgr ⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
5 iscusgr ⊢ ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplUSGraph ↔ ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph ∧ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplGraph ) )
6 3 4 5 3imtr4i ⊢ ( 𝐺 ∈ ComplUSGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplUSGraph )