Theorem vtxdlfuhgr1v

Description: The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021)

	Ref	Expression
Hypotheses	vtxdlfuhgr1v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdlfuhgr1v.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	vtxdlfuhgr1v.e	⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
Assertion	vtxdlfuhgr1v	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdlfuhgr1v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdlfuhgr1v.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		vtxdlfuhgr1v.e	⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
4		simpl1	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) ∧ 𝑈 ∈ 𝑉 ) → 𝐺 ∈ UHGraph )
5		simpr	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) ∧ 𝑈 ∈ 𝑉 ) → 𝑈 ∈ 𝑉 )
6	1 2 3	lfuhgr1v0e	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( Edg ‘ 𝐺 ) = ∅ )
7	6	adantr	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) ∧ 𝑈 ∈ 𝑉 ) → ( Edg ‘ 𝐺 ) = ∅ )
8		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
9	1 8	vtxduhgr0e	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ ( Edg ‘ 𝐺 ) = ∅ ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )
10	4 5 7 9	syl3anc	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 )
11	10	ex	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐼 : dom 𝐼 ⟶ 𝐸 ) → ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ) )