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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vdn0conngrumgrv2 ( ( ( 𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph ) ∧ ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 0 )

Proof

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