rusgrprop

Description: The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 18-Dec-2020)

		Ref	Expression
	Assertion	rusgrprop	$⊢ G RegUSGraph K \to (G \in USGraph \land G RegGraph K)$

Step	Hyp	Ref	Expression
1		df-rusgr	$⊢ RegUSGraph = \{⟨g, k⟩ \| (g \in USGraph \land g RegGraph k)\}$
2	1	bropaex12	$⊢ G RegUSGraph K \to (G \in V \land K \in V)$
3		isrusgr	$⊢ (G \in V \land K \in V) \to (G RegUSGraph K \leftrightarrow (G \in USGraph \land G RegGraph K))$
4	3	biimpd	$⊢ (G \in V \land K \in V) \to (G RegUSGraph K \to (G \in USGraph \land G RegGraph K))$
5	2 4	mpcom	$⊢ G RegUSGraph K \to (G \in USGraph \land G RegGraph K)$

Metamath Proof Explorer