Metamath Proof Explorer

Theorem 1egrvtxdg1

Description: The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other 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 ⁡ G = V
1egrvtxdg1.a ⊢ φ → A ∈ X
1egrvtxdg1.b ⊢ φ → B ∈ V
1egrvtxdg1.c ⊢ φ → C ∈ V
1egrvtxdg1.n ⊢ φ → B ≠ C
1egrvtxdg1.i ⊢ φ → iEdg ⁡ G = A B C
Assertion 1egrvtxdg1 ⊢ φ → VtxDeg ⁡ G ⁡ B = 1

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 1egrvtxdg1.i ⊢ φ → iEdg ⁡ G = A B C
7 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
8 3 1 eleqtrrd ⊢ φ → B ∈ Vtx ⁡ G
9 4 1 eleqtrrd ⊢ φ → C ∈ Vtx ⁡ G
10 7 2 8 9 6 5 usgr1e ⊢ φ → G ∈ USGraph
11 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
12 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
13 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
14 7 11 12 13 vtxdusgrval ⊢ G ∈ USGraph ∧ B ∈ Vtx ⁡ G → VtxDeg ⁡ G ⁡ B = x ∈ dom ⁡ iEdg ⁡ G | B ∈ iEdg ⁡ G ⁡ x
15 10 8 14 syl2anc ⊢ φ → VtxDeg ⁡ G ⁡ B = x ∈ dom ⁡ iEdg ⁡ G | B ∈ iEdg ⁡ G ⁡ x
16 dmeq ⊢ iEdg ⁡ G = A B C → dom ⁡ iEdg ⁡ G = dom ⁡ A B C
17 16 adantl ⊢ φ ∧ iEdg ⁡ G = A B C → dom ⁡ iEdg ⁡ G = dom ⁡ A B C
18 prex ⊢ B C ∈ V
19 dmsnopg ⊢ B C ∈ V → dom ⁡ A B C = A
20 18 19 mp1i ⊢ φ ∧ iEdg ⁡ G = A B C → dom ⁡ A B C = A
21 17 20 eqtrd ⊢ φ ∧ iEdg ⁡ G = A B C → dom ⁡ iEdg ⁡ G = A
22 fveq1 ⊢ iEdg ⁡ G = A B C → iEdg ⁡ G ⁡ x = A B C ⁡ x
23 22 eleq2d ⊢ iEdg ⁡ G = A B C → B ∈ iEdg ⁡ G ⁡ x ↔ B ∈ A B C ⁡ x
24 23 adantl ⊢ φ ∧ iEdg ⁡ G = A B C → B ∈ iEdg ⁡ G ⁡ x ↔ B ∈ A B C ⁡ x
25 21 24 rabeqbidv ⊢ φ ∧ iEdg ⁡ G = A B C → x ∈ dom ⁡ iEdg ⁡ G | B ∈ iEdg ⁡ G ⁡ x = x ∈ A | B ∈ A B C ⁡ x
26 25 fveq2d ⊢ φ ∧ iEdg ⁡ G = A B C → x ∈ dom ⁡ iEdg ⁡ G | B ∈ iEdg ⁡ G ⁡ x = x ∈ A | B ∈ A B C ⁡ x
27 fveq2 ⊢ x = A → A B C ⁡ x = A B C ⁡ A
28 27 eleq2d ⊢ x = A → B ∈ A B C ⁡ x ↔ B ∈ A B C ⁡ A
29 28 rabsnif ⊢ x ∈ A | B ∈ A B C ⁡ x = if B ∈ A B C ⁡ A A ∅
30 prid1g ⊢ B ∈ V → B ∈ B C
31 3 30 syl ⊢ φ → B ∈ B C
32 fvsng ⊢ A ∈ X ∧ B C ∈ V → A B C ⁡ A = B C
33 2 18 32 sylancl ⊢ φ → A B C ⁡ A = B C
34 31 33 eleqtrrd ⊢ φ → B ∈ A B C ⁡ A
35 34 iftrued ⊢ φ → if B ∈ A B C ⁡ A A ∅ = A
36 29 35 syl5eq ⊢ φ → x ∈ A | B ∈ A B C ⁡ x = A
37 36 fveq2d ⊢ φ → x ∈ A | B ∈ A B C ⁡ x = A
38 hashsng ⊢ A ∈ X → A = 1
39 2 38 syl ⊢ φ → A = 1
40 37 39 eqtrd ⊢ φ → x ∈ A | B ∈ A B C ⁡ x = 1
41 40 adantr ⊢ φ ∧ iEdg ⁡ G = A B C → x ∈ A | B ∈ A B C ⁡ x = 1
42 26 41 eqtrd ⊢ φ ∧ iEdg ⁡ G = A B C → x ∈ dom ⁡ iEdg ⁡ G | B ∈ iEdg ⁡ G ⁡ x = 1
43 6 42 mpdan ⊢ φ → x ∈ dom ⁡ iEdg ⁡ G | B ∈ iEdg ⁡ G ⁡ x = 1
44 15 43 eqtrd ⊢ φ → VtxDeg ⁡ G ⁡ B = 1