1egrvtxdg1r

Description: The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given 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, 21-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		1egrvtxdg1.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2		1egrvtxdg1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		1egrvtxdg1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		1egrvtxdg1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		1egrvtxdg1.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
6		1egrvtxdg1.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
7	5	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
8		prcom	⊢ { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 }
9	8	a1i	⊢ ( 𝜑 → { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 } )
10	9	opeq2d	⊢ ( 𝜑 → ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ = ⟨ 𝐴 , { 𝐶 , 𝐵 } ⟩ )
11	10	sneqd	⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { ⟨ 𝐴 , { 𝐶 , 𝐵 } ⟩ } )
12	6 11	eqtrd	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐶 , 𝐵 } ⟩ } )
13	1 2 4 3 7 12	1egrvtxdg1	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 1 )

Metamath Proof Explorer

Theorem 1egrvtxdg1r

Proof