# Metamath Proof Explorer

## Theorem 1egrvtxdg0

Description: The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex 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 ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\right)={V}$
1egrvtxdg1.a ${⊢}{\phi }\to {A}\in {X}$
1egrvtxdg1.b ${⊢}{\phi }\to {B}\in {V}$
1egrvtxdg1.c ${⊢}{\phi }\to {C}\in {V}$
1egrvtxdg1.n ${⊢}{\phi }\to {B}\ne {C}$
1egrvtxdg0.d ${⊢}{\phi }\to {D}\in {V}$
1egrvtxdg0.n ${⊢}{\phi }\to {C}\ne {D}$
1egrvtxdg0.i ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}$
Assertion 1egrvtxdg0 ${⊢}{\phi }\to \mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0$

### Proof

Step Hyp Ref Expression
1 1egrvtxdg1.v ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\right)={V}$
2 1egrvtxdg1.a ${⊢}{\phi }\to {A}\in {X}$
3 1egrvtxdg1.b ${⊢}{\phi }\to {B}\in {V}$
4 1egrvtxdg1.c ${⊢}{\phi }\to {C}\in {V}$
5 1egrvtxdg1.n ${⊢}{\phi }\to {B}\ne {C}$
6 1egrvtxdg0.d ${⊢}{\phi }\to {D}\in {V}$
7 1egrvtxdg0.n ${⊢}{\phi }\to {C}\ne {D}$
8 1egrvtxdg0.i ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}$
9 1 adantl ${⊢}\left({B}={D}\wedge {\phi }\right)\to \mathrm{Vtx}\left({G}\right)={V}$
10 2 adantl ${⊢}\left({B}={D}\wedge {\phi }\right)\to {A}\in {X}$
11 3 adantl ${⊢}\left({B}={D}\wedge {\phi }\right)\to {B}\in {V}$
12 8 adantl ${⊢}\left({B}={D}\wedge {\phi }\right)\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}$
13 preq2 ${⊢}{D}={B}\to \left\{{B},{D}\right\}=\left\{{B},{B}\right\}$
14 13 eqcoms ${⊢}{B}={D}\to \left\{{B},{D}\right\}=\left\{{B},{B}\right\}$
15 dfsn2 ${⊢}\left\{{B}\right\}=\left\{{B},{B}\right\}$
16 14 15 syl6eqr ${⊢}{B}={D}\to \left\{{B},{D}\right\}=\left\{{B}\right\}$
17 16 adantr ${⊢}\left({B}={D}\wedge {\phi }\right)\to \left\{{B},{D}\right\}=\left\{{B}\right\}$
18 17 opeq2d ${⊢}\left({B}={D}\wedge {\phi }\right)\to ⟨{A},\left\{{B},{D}\right\}⟩=⟨{A},\left\{{B}\right\}⟩$
19 18 sneqd ${⊢}\left({B}={D}\wedge {\phi }\right)\to \left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}=\left\{⟨{A},\left\{{B}\right\}⟩\right\}$
20 12 19 eqtrd ${⊢}\left({B}={D}\wedge {\phi }\right)\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B}\right\}⟩\right\}$
21 5 necomd ${⊢}{\phi }\to {C}\ne {B}$
22 4 21 jca ${⊢}{\phi }\to \left({C}\in {V}\wedge {C}\ne {B}\right)$
23 eldifsn ${⊢}{C}\in \left({V}\setminus \left\{{B}\right\}\right)↔\left({C}\in {V}\wedge {C}\ne {B}\right)$
24 22 23 sylibr ${⊢}{\phi }\to {C}\in \left({V}\setminus \left\{{B}\right\}\right)$
25 24 adantl ${⊢}\left({B}={D}\wedge {\phi }\right)\to {C}\in \left({V}\setminus \left\{{B}\right\}\right)$
26 9 10 11 20 25 1loopgrvd0 ${⊢}\left({B}={D}\wedge {\phi }\right)\to \mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0$
27 26 ex ${⊢}{B}={D}\to \left({\phi }\to \mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0\right)$
28 necom ${⊢}{B}\ne {C}↔{C}\ne {B}$
29 df-ne ${⊢}{C}\ne {B}↔¬{C}={B}$
30 28 29 sylbb ${⊢}{B}\ne {C}\to ¬{C}={B}$
31 5 30 syl ${⊢}{\phi }\to ¬{C}={B}$
32 7 neneqd ${⊢}{\phi }\to ¬{C}={D}$
33 31 32 jca ${⊢}{\phi }\to \left(¬{C}={B}\wedge ¬{C}={D}\right)$
34 33 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \left(¬{C}={B}\wedge ¬{C}={D}\right)$
35 ioran ${⊢}¬\left({C}={B}\vee {C}={D}\right)↔\left(¬{C}={B}\wedge ¬{C}={D}\right)$
36 34 35 sylibr ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to ¬\left({C}={B}\vee {C}={D}\right)$
37 edgval ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
38 8 rneqd ${⊢}{\phi }\to \mathrm{ran}\mathrm{iEdg}\left({G}\right)=\mathrm{ran}\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}$
39 rnsnopg ${⊢}{A}\in {X}\to \mathrm{ran}\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}=\left\{\left\{{B},{D}\right\}\right\}$
40 2 39 syl ${⊢}{\phi }\to \mathrm{ran}\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}=\left\{\left\{{B},{D}\right\}\right\}$
41 38 40 eqtrd ${⊢}{\phi }\to \mathrm{ran}\mathrm{iEdg}\left({G}\right)=\left\{\left\{{B},{D}\right\}\right\}$
42 37 41 syl5eq ${⊢}{\phi }\to \mathrm{Edg}\left({G}\right)=\left\{\left\{{B},{D}\right\}\right\}$
43 42 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \mathrm{Edg}\left({G}\right)=\left\{\left\{{B},{D}\right\}\right\}$
44 43 rexeqdv ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \left(\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{C}\in {e}↔\exists {e}\in \left\{\left\{{B},{D}\right\}\right\}\phantom{\rule{.4em}{0ex}}{C}\in {e}\right)$
45 prex ${⊢}\left\{{B},{D}\right\}\in \mathrm{V}$
46 eleq2 ${⊢}{e}=\left\{{B},{D}\right\}\to \left({C}\in {e}↔{C}\in \left\{{B},{D}\right\}\right)$
47 46 rexsng ${⊢}\left\{{B},{D}\right\}\in \mathrm{V}\to \left(\exists {e}\in \left\{\left\{{B},{D}\right\}\right\}\phantom{\rule{.4em}{0ex}}{C}\in {e}↔{C}\in \left\{{B},{D}\right\}\right)$
48 45 47 mp1i ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \left(\exists {e}\in \left\{\left\{{B},{D}\right\}\right\}\phantom{\rule{.4em}{0ex}}{C}\in {e}↔{C}\in \left\{{B},{D}\right\}\right)$
49 elprg ${⊢}{C}\in {V}\to \left({C}\in \left\{{B},{D}\right\}↔\left({C}={B}\vee {C}={D}\right)\right)$
50 4 49 syl ${⊢}{\phi }\to \left({C}\in \left\{{B},{D}\right\}↔\left({C}={B}\vee {C}={D}\right)\right)$
51 50 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \left({C}\in \left\{{B},{D}\right\}↔\left({C}={B}\vee {C}={D}\right)\right)$
52 44 48 51 3bitrd ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \left(\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{C}\in {e}↔\left({C}={B}\vee {C}={D}\right)\right)$
53 36 52 mtbird ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to ¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{C}\in {e}$
54 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
55 2 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to {A}\in {X}$
56 3 1 eleqtrrd ${⊢}{\phi }\to {B}\in \mathrm{Vtx}\left({G}\right)$
57 56 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to {B}\in \mathrm{Vtx}\left({G}\right)$
58 6 1 eleqtrrd ${⊢}{\phi }\to {D}\in \mathrm{Vtx}\left({G}\right)$
59 58 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to {D}\in \mathrm{Vtx}\left({G}\right)$
60 8 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B},{D}\right\}⟩\right\}$
61 simpl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to {B}\ne {D}$
62 54 55 57 59 60 61 usgr1e ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to {G}\in \mathrm{USGraph}$
63 4 1 eleqtrrd ${⊢}{\phi }\to {C}\in \mathrm{Vtx}\left({G}\right)$
64 63 adantl ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to {C}\in \mathrm{Vtx}\left({G}\right)$
65 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
66 eqid ${⊢}\mathrm{VtxDeg}\left({G}\right)=\mathrm{VtxDeg}\left({G}\right)$
67 54 65 66 vtxdusgr0edgnel ${⊢}\left({G}\in \mathrm{USGraph}\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\to \left(\mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0↔¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{C}\in {e}\right)$
68 62 64 67 syl2anc ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \left(\mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0↔¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{C}\in {e}\right)$
69 53 68 mpbird ${⊢}\left({B}\ne {D}\wedge {\phi }\right)\to \mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0$
70 69 ex ${⊢}{B}\ne {D}\to \left({\phi }\to \mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0\right)$
71 27 70 pm2.61ine ${⊢}{\phi }\to \mathrm{VtxDeg}\left({G}\right)\left({C}\right)=0$