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	⊢ ( 𝐺 ∈ USGraph → ( 𝐺 RegUSGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		isrusgr	⊢ ( ( 𝐺 ∈ USGraph ∧ 0 ∈ ℕ0 ) → ( 𝐺 RegUSGraph 0 ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 RegGraph 0 ) ) )
3	1 2	mpan2	⊢ ( 𝐺 ∈ USGraph → ( 𝐺 RegUSGraph 0 ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 RegGraph 0 ) ) )
4		ibar	⊢ ( 𝐺 ∈ USGraph → ( 𝐺 RegGraph 0 ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 RegGraph 0 ) ) )
5		usgruhgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
6		uhgr0edg0rgrb	⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 RegGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )
7	5 6	syl	⊢ ( 𝐺 ∈ USGraph → ( 𝐺 RegGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )
8	3 4 7	3bitr2d	⊢ ( 𝐺 ∈ USGraph → ( 𝐺 RegUSGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )