Metamath Proof Explorer

Theorem usgr0edg0rusgr

Description: A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 19-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

		Ref	Expression
	Assertion	usgr0edg0rusgr	$⊢ G \in USGraph \to (G RegUSGraph 0 \leftrightarrow Edg (G) = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		isrusgr	$⊢ (G \in USGraph \land 0 \in ℕ_{0}) \to (G RegUSGraph 0 \leftrightarrow (G \in USGraph \land G RegGraph 0))$
3	1 2	mpan2	$⊢ G \in USGraph \to (G RegUSGraph 0 \leftrightarrow (G \in USGraph \land G RegGraph 0))$
4		ibar	$⊢ G \in USGraph \to (G RegGraph 0 \leftrightarrow (G \in USGraph \land G RegGraph 0))$
5		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
6		uhgr0edg0rgrb	$⊢ G \in UHGraph \to (G RegGraph 0 \leftrightarrow Edg (G) = \emptyset)$
7	5 6	syl	$⊢ G \in USGraph \to (G RegGraph 0 \leftrightarrow Edg (G) = \emptyset)$
8	3 4 7	3bitr2d	$⊢ G \in USGraph \to (G RegUSGraph 0 \leftrightarrow Edg (G) = \emptyset)$