Metamath Proof Explorer

Theorem vdn0conngrumgrv2

Description: A vertex in a connected multigraph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

Ref Expression
Hypothesis vdn0conngrv2.v ⊢ V = Vtx ⁡ G
Assertion vdn0conngrumgrv2 ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → VtxDeg ⁡ G ⁡ N ≠ 0

Proof

Step Hyp Ref Expression
1 vdn0conngrv2.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
4 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
5 1 2 3 4 vtxdumgrval ⊢ G ∈ UMGraph ∧ N ∈ V → VtxDeg ⁡ G ⁡ N = x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x
6 5 ad2ant2lr ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → VtxDeg ⁡ G ⁡ N = x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x
7 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
8 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
9 funfn ⊢ Fun ⁡ iEdg ⁡ G ↔ iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
10 9 biimpi ⊢ Fun ⁡ iEdg ⁡ G → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
11 7 8 10 3syl ⊢ G ∈ UMGraph → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
12 11 adantl ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
13 12 adantr ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
14 simpl ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph → G ∈ ConnGraph
15 14 adantr ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → G ∈ ConnGraph
16 simpl ⊢ N ∈ V ∧ 1 < V → N ∈ V
17 16 adantl ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → N ∈ V
18 simprr ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → 1 < V
19 1 2 conngrv2edg ⊢ G ∈ ConnGraph ∧ N ∈ V ∧ 1 < V → ∃ e ∈ ran ⁡ iEdg ⁡ G N ∈ e
20 15 17 18 19 syl3anc ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → ∃ e ∈ ran ⁡ iEdg ⁡ G N ∈ e
21 eleq2 ⊢ e = iEdg ⁡ G ⁡ x → N ∈ e ↔ N ∈ iEdg ⁡ G ⁡ x
22 21 rexrn ⊢ iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G → ∃ e ∈ ran ⁡ iEdg ⁡ G N ∈ e ↔ ∃ x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
23 22 biimpd ⊢ iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G → ∃ e ∈ ran ⁡ iEdg ⁡ G N ∈ e → ∃ x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
24 13 20 23 sylc ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → ∃ x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
25 dfrex2 ⊢ ∃ x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x ↔ ¬ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ N ∈ iEdg ⁡ G ⁡ x
26 24 25 sylib ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → ¬ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ N ∈ iEdg ⁡ G ⁡ x
27 fvex ⊢ iEdg ⁡ G ∈ V
28 27 dmex ⊢ dom ⁡ iEdg ⁡ G ∈ V
29 28 a1i ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → dom ⁡ iEdg ⁡ G ∈ V
30 rabexg ⊢ dom ⁡ iEdg ⁡ G ∈ V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x ∈ V
31 hasheq0 ⊢ x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x ∈ V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = 0 ↔ x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = ∅
32 29 30 31 3syl ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = 0 ↔ x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = ∅
33 rabeq0 ⊢ x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = ∅ ↔ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ N ∈ iEdg ⁡ G ⁡ x
34 32 33 syl6bb ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = 0 ↔ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ N ∈ iEdg ⁡ G ⁡ x
35 34 necon3abid ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x ≠ 0 ↔ ¬ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ N ∈ iEdg ⁡ G ⁡ x
36 26 35 mpbird ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x ≠ 0
37 6 36 eqnetrd ⊢ G ∈ ConnGraph ∧ G ∈ UMGraph ∧ N ∈ V ∧ 1 < V → VtxDeg ⁡ G ⁡ N ≠ 0