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