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 ⊢ V = Vtx ⁡ G
vtxdlfuhgr1v.i ⊢ I = iEdg ⁡ G
vtxdlfuhgr1v.e ⊢ E = x ∈ 𝒫 V | 2 ≤ x
Assertion vtxdlfuhgr1v ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E → U ∈ V → VtxDeg ⁡ G ⁡ U = 0

Proof

Step Hyp Ref Expression
1 vtxdlfuhgr1v.v ⊢ V = Vtx ⁡ G
2 vtxdlfuhgr1v.i ⊢ I = iEdg ⁡ G
3 vtxdlfuhgr1v.e ⊢ E = x ∈ 𝒫 V | 2 ≤ x
4 simpl1 ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E ∧ U ∈ V → G ∈ UHGraph
5 simpr ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E ∧ U ∈ V → U ∈ V
6 1 2 3 lfuhgr1v0e ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E → Edg ⁡ G = ∅
7 6 adantr ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E ∧ U ∈ V → Edg ⁡ G = ∅
8 eqid ⊢ Edg ⁡ G = Edg ⁡ G
9 1 8 vtxduhgr0e ⊢ G ∈ UHGraph ∧ U ∈ V ∧ Edg ⁡ G = ∅ → VtxDeg ⁡ G ⁡ U = 0
10 4 5 7 9 syl3anc ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = 0
11 10 ex ⊢ G ∈ UHGraph ∧ V = 1 ∧ I : dom ⁡ I ⟶ E → U ∈ V → VtxDeg ⁡ G ⁡ U = 0