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 )