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