This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtxduhgr0e

Description: The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e . (Contributed by AV, 15-Dec-2020)

Ref Expression
Hypotheses vtxduhgr0e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxduhgr0e.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion vtxduhgr0e ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )

Proof

Step Hyp Ref Expression
1 vtxduhgr0e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxduhgr0e.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 3 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
5 3 2 edg0iedg0 ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
6 4 5 syl ⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
7 6 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
8 1 3 vtxdg0e ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )
9 8 ex ⊢ ( 𝑈 ∈ 𝑉 → ( ( iEdg ‘ 𝐺 ) = ∅ → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ) )
10 9 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( iEdg ‘ 𝐺 ) = ∅ → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ) )
11 7 10 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐸 = ∅ → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ) )
12 11 3impia ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )