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 )