Metamath Proof Explorer


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