# 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}=\mathrm{Vtx}\left({G}\right)$
vtxdusgradjvtx.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion uhgrvd00 ${⊢}{G}\in \mathrm{UHGraph}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=0\to {E}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 vtxdusgradjvtx.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 eqid ${⊢}\mathrm{VtxDeg}\left({G}\right)=\mathrm{VtxDeg}\left({G}\right)$
4 1 2 3 vtxduhgr0edgnel ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {v}\in {V}\right)\to \left(\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=0↔¬\exists {e}\in {E}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
5 ralnex ${⊢}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}↔¬\exists {e}\in {E}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
6 4 5 syl6bbr ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {v}\in {V}\right)\to \left(\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=0↔\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}\right)$
7 6 ralbidva ${⊢}{G}\in \mathrm{UHGraph}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=0↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}\right)$
8 ralcom ${⊢}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}↔\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}$
9 ralnex2 ${⊢}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}↔¬\exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
10 8 9 bitri ${⊢}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}↔¬\exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
11 simpr ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {e}\in {E}\right)\to {e}\in {E}$
12 2 eleq2i ${⊢}{e}\in {E}↔{e}\in \mathrm{Edg}\left({G}\right)$
13 uhgredgn0 ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {e}\in \mathrm{Edg}\left({G}\right)\right)\to {e}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)$
14 12 13 sylan2b ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {e}\in {E}\right)\to {e}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)$
15 eldifsn ${⊢}{e}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)↔\left({e}\in 𝒫\mathrm{Vtx}\left({G}\right)\wedge {e}\ne \varnothing \right)$
16 elpwi ${⊢}{e}\in 𝒫\mathrm{Vtx}\left({G}\right)\to {e}\subseteq \mathrm{Vtx}\left({G}\right)$
17 1 sseq2i ${⊢}{e}\subseteq {V}↔{e}\subseteq \mathrm{Vtx}\left({G}\right)$
18 ssn0rex ${⊢}\left({e}\subseteq {V}\wedge {e}\ne \varnothing \right)\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
19 18 ex ${⊢}{e}\subseteq {V}\to \left({e}\ne \varnothing \to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
20 17 19 sylbir ${⊢}{e}\subseteq \mathrm{Vtx}\left({G}\right)\to \left({e}\ne \varnothing \to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
21 16 20 syl ${⊢}{e}\in 𝒫\mathrm{Vtx}\left({G}\right)\to \left({e}\ne \varnothing \to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
22 21 imp ${⊢}\left({e}\in 𝒫\mathrm{Vtx}\left({G}\right)\wedge {e}\ne \varnothing \right)\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
23 15 22 sylbi ${⊢}{e}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
24 14 23 syl ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {e}\in {E}\right)\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}$
25 11 24 jca ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {e}\in {E}\right)\to \left({e}\in {E}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
26 25 ex ${⊢}{G}\in \mathrm{UHGraph}\to \left({e}\in {E}\to \left({e}\in {E}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)\right)$
27 26 eximdv ${⊢}{G}\in \mathrm{UHGraph}\to \left(\exists {e}\phantom{\rule{.4em}{0ex}}{e}\in {E}\to \exists {e}\phantom{\rule{.4em}{0ex}}\left({e}\in {E}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)\right)$
28 n0 ${⊢}{E}\ne \varnothing ↔\exists {e}\phantom{\rule{.4em}{0ex}}{e}\in {E}$
29 df-rex ${⊢}\exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}↔\exists {e}\phantom{\rule{.4em}{0ex}}\left({e}\in {E}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
30 27 28 29 3imtr4g ${⊢}{G}\in \mathrm{UHGraph}\to \left({E}\ne \varnothing \to \exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\right)$
31 30 con3d ${⊢}{G}\in \mathrm{UHGraph}\to \left(¬\exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}\in {e}\to ¬{E}\ne \varnothing \right)$
32 10 31 syl5bi ${⊢}{G}\in \mathrm{UHGraph}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}\to ¬{E}\ne \varnothing \right)$
33 nne ${⊢}¬{E}\ne \varnothing ↔{E}=\varnothing$
34 32 33 syl6ib ${⊢}{G}\in \mathrm{UHGraph}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {e}\in {E}\phantom{\rule{.4em}{0ex}}¬{v}\in {e}\to {E}=\varnothing \right)$
35 7 34 sylbid ${⊢}{G}\in \mathrm{UHGraph}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=0\to {E}=\varnothing \right)$