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 = ∅