cusgrop

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

		Ref	Expression
	Assertion	cusgrop	$⊢ G \in ComplUSGraph \to ⟨Vtx (G), iEdg (G)⟩ \in ComplUSGraph$

Step	Hyp	Ref	Expression
1		usgrop	$⊢ G \in USGraph \to ⟨Vtx (G), iEdg (G)⟩ \in USGraph$
2		cplgrop	$⊢ G \in ComplGraph \to ⟨Vtx (G), iEdg (G)⟩ \in ComplGraph$
3	1 2	anim12i	$⊢ (G \in USGraph \land G \in ComplGraph) \to (⟨Vtx (G), iEdg (G)⟩ \in USGraph \land ⟨Vtx (G), iEdg (G)⟩ \in ComplGraph)$
4		iscusgr	$⊢ G \in ComplUSGraph \leftrightarrow (G \in USGraph \land G \in ComplGraph)$
5		iscusgr	$⊢ ⟨Vtx (G), iEdg (G)⟩ \in ComplUSGraph \leftrightarrow (⟨Vtx (G), iEdg (G)⟩ \in USGraph \land ⟨Vtx (G), iEdg (G)⟩ \in ComplGraph)$
6	3 4 5	3imtr4i	$⊢ G \in ComplUSGraph \to ⟨Vtx (G), iEdg (G)⟩ \in ComplUSGraph$

Metamath Proof Explorer