Metamath Proof Explorer

Theorem uhgr0edg0rgrb

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

Ref Expression
Assertion uhgr0edg0rgrb ( 𝐺 ∈ UHGraph → ( 𝐺 RegGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 uhgrvd00 ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → ( Edg ‘ 𝐺 ) = ∅ ) )
4 3 com12 ⊢ ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) = ∅ ) )
5 4 adantl ⊢ ( ( 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ) → ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) = ∅ ) )
6 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
7 1 6 rgrprop ⊢ ( 𝐺 RegGraph 0 → ( 0 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ) )
8 5 7 syl11 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 RegGraph 0 → ( Edg ‘ 𝐺 ) = ∅ ) )
9 uhgr0edg0rgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Edg ‘ 𝐺 ) = ∅ ) → 𝐺 RegGraph 0 )
10 9 ex ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ → 𝐺 RegGraph 0 ) )
11 8 10 impbid ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 RegGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )