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

Metamath Proof Explorer

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 ) )