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 φ Vtx G = V
1egrvtxdg1.a φ A X
1egrvtxdg1.b φ B V
1egrvtxdg1.c φ C V
1egrvtxdg1.n φ B C
1egrvtxdg0.d φ D V
1egrvtxdg0.n φ C D
1egrvtxdg0.i φ iEdg G = A B D
Assertion 1egrvtxdg0 φ VtxDeg G C = 0

Proof

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