Metamath Proof Explorer

Theorem uhgrvd00

Description: If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdusgradjvtx.v ⊢V=Vtx⁡G
vtxdusgradjvtx.e ⊢E=Edg⁡G
Assertion uhgrvd00 ⊢G∈UHGraph→∀v∈VVtxDeg⁡G⁡v=0→E=∅

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v ⊢V=Vtx⁡G
2 vtxdusgradjvtx.e ⊢E=Edg⁡G
3 eqid ⊢VtxDeg⁡G=VtxDeg⁡G
4 1 2 3 vtxduhgr0edgnel ⊢G∈UHGraph∧v∈V→VtxDeg⁡G⁡v=0↔¬∃e∈Ev∈e
5 ralnex ⊢∀e∈E¬v∈e↔¬∃e∈Ev∈e
6 4 5 bitr4di ⊢G∈UHGraph∧v∈V→VtxDeg⁡G⁡v=0↔∀e∈E¬v∈e
7 6 ralbidva ⊢G∈UHGraph→∀v∈VVtxDeg⁡G⁡v=0↔∀v∈V∀e∈E¬v∈e
8 ralcom ⊢∀v∈V∀e∈E¬v∈e↔∀e∈E∀v∈V¬v∈e
9 ralnex2 ⊢∀e∈E∀v∈V¬v∈e↔¬∃e∈E∃v∈Vv∈e
10 8 9 bitri ⊢∀v∈V∀e∈E¬v∈e↔¬∃e∈E∃v∈Vv∈e
11 simpr ⊢G∈UHGraph∧e∈E→e∈E
12 2 eleq2i ⊢e∈E↔e∈Edg⁡G
13 uhgredgn0 ⊢G∈UHGraph∧e∈Edg⁡G→e∈𝒫Vtx⁡G∖∅
14 12 13 sylan2b ⊢G∈UHGraph∧e∈E→e∈𝒫Vtx⁡G∖∅
15 eldifsn ⊢e∈𝒫Vtx⁡G∖∅↔e∈𝒫Vtx⁡G∧e≠∅
16 elpwi ⊢e∈𝒫Vtx⁡G→e⊆Vtx⁡G
17 1 sseq2i ⊢e⊆V↔e⊆Vtx⁡G
18 ssn0rex ⊢e⊆V∧e≠∅→∃v∈Vv∈e
19 18 ex ⊢e⊆V→e≠∅→∃v∈Vv∈e
20 17 19 sylbir ⊢e⊆Vtx⁡G→e≠∅→∃v∈Vv∈e
21 16 20 syl ⊢e∈𝒫Vtx⁡G→e≠∅→∃v∈Vv∈e
22 21 imp ⊢e∈𝒫Vtx⁡G∧e≠∅→∃v∈Vv∈e
23 15 22 sylbi ⊢e∈𝒫Vtx⁡G∖∅→∃v∈Vv∈e
24 14 23 syl ⊢G∈UHGraph∧e∈E→∃v∈Vv∈e
25 11 24 jca ⊢G∈UHGraph∧e∈E→e∈E∧∃v∈Vv∈e
26 25 ex ⊢G∈UHGraph→e∈E→e∈E∧∃v∈Vv∈e
27 26 eximdv ⊢G∈UHGraph→∃ee∈E→∃ee∈E∧∃v∈Vv∈e
28 n0 ⊢E≠∅↔∃ee∈E
29 df-rex ⊢∃e∈E∃v∈Vv∈e↔∃ee∈E∧∃v∈Vv∈e
30 27 28 29 3imtr4g ⊢G∈UHGraph→E≠∅→∃e∈E∃v∈Vv∈e
31 30 con3d ⊢G∈UHGraph→¬∃e∈E∃v∈Vv∈e→¬E≠∅
32 10 31 biimtrid ⊢G∈UHGraph→∀v∈V∀e∈E¬v∈e→¬E≠∅
33 nne ⊢¬E≠∅↔E=∅
34 32 33 imbitrdi ⊢G∈UHGraph→∀v∈V∀e∈E¬v∈e→E=∅
35 7 34 sylbid ⊢G∈UHGraph→∀v∈VVtxDeg⁡G⁡v=0→E=∅