1hegrvtxdg1

Description: The vertex degree of a graph with one hyperedge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	1hegrvtxdg1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	1hegrvtxdg1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	1hegrvtxdg1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	1hegrvtxdg1.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	1hegrvtxdg1.x	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
	1hegrvtxdg1.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
	1hegrvtxdg1.e	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝐸 )
	1hegrvtxdg1.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
Assertion	1hegrvtxdg1	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1hegrvtxdg1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
2		1hegrvtxdg1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		1hegrvtxdg1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		1hegrvtxdg1.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
5		1hegrvtxdg1.x	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
6		1hegrvtxdg1.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
7		1hegrvtxdg1.e	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝐸 )
8		1hegrvtxdg1.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
9		prid1g	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 , 𝐶 } )
10	2 9	syl	⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 , 𝐶 } )
11	7 10	sseldd	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
12		prid2g	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ { 𝐵 , 𝐶 } )
13	3 12	syl	⊢ ( 𝜑 → 𝐶 ∈ { 𝐵 , 𝐶 } )
14	7 13	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝐸 )
15	5 11 14 4	nehash2	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
16	6 8 1 2 5 11 15	1hevtxdg1	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )

Metamath Proof Explorer

Theorem 1hegrvtxdg1

Proof