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 V VtxDeg 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 E v e
5 ralnex e E ¬ v e ¬ e E v e
6 4 5 bitr4di G UHGraph v V VtxDeg G v = 0 e E ¬ v e
7 6 ralbidva G UHGraph v V VtxDeg 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 V v e
10 8 9 bitri v V e E ¬ v e ¬ e E v V v 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 V v e
19 18 ex e V e v V v e
20 17 19 sylbir e Vtx G e v V v e
21 16 20 syl e 𝒫 Vtx G e v V v e
22 21 imp e 𝒫 Vtx G e v V v e
23 15 22 sylbi e 𝒫 Vtx G v V v e
24 14 23 syl G UHGraph e E v V v e
25 11 24 jca G UHGraph e E e E v V v e
26 25 ex G UHGraph e E e E v V v e
27 26 eximdv G UHGraph e e E e e E v V v e
28 n0 E e e E
29 df-rex e E v V v e e e E v V v e
30 27 28 29 3imtr4g G UHGraph E e E v V v e
31 30 con3d G UHGraph ¬ e E v V v e ¬ E
32 10 31 syl5bi G UHGraph v V e E ¬ v e ¬ E
33 nne ¬ E E =
34 32 33 syl6ib G UHGraph v V e E ¬ v e E =
35 7 34 sylbid G UHGraph v V VtxDeg G v = 0 E =