Metamath Proof Explorer

Theorem 1loopgrvd0

Description: The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v ⊢ φ → Vtx ⁡ G = V
1loopgruspgr.a ⊢ φ → A ∈ X
1loopgruspgr.n ⊢ φ → N ∈ V
1loopgruspgr.i ⊢ φ → iEdg ⁡ G = A N
1loopgrvd0.k ⊢ φ → K ∈ V ∖ N
Assertion 1loopgrvd0 ⊢ φ → VtxDeg ⁡ G ⁡ K = 0

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v ⊢ φ → Vtx ⁡ G = V
2 1loopgruspgr.a ⊢ φ → A ∈ X
3 1loopgruspgr.n ⊢ φ → N ∈ V
4 1loopgruspgr.i ⊢ φ → iEdg ⁡ G = A N
5 1loopgrvd0.k ⊢ φ → K ∈ V ∖ N
6 5 eldifbd ⊢ φ → ¬ K ∈ N
7 snex ⊢ N ∈ V
8 fvsng ⊢ A ∈ X ∧ N ∈ V → A N ⁡ A = N
9 2 7 8 sylancl ⊢ φ → A N ⁡ A = N
10 9 eleq2d ⊢ φ → K ∈ A N ⁡ A ↔ K ∈ N
11 6 10 mtbird ⊢ φ → ¬ K ∈ A N ⁡ A
12 4 dmeqd ⊢ φ → dom ⁡ iEdg ⁡ G = dom ⁡ A N
13 dmsnopg ⊢ N ∈ V → dom ⁡ A N = A
14 7 13 mp1i ⊢ φ → dom ⁡ A N = A
15 12 14 eqtrd ⊢ φ → dom ⁡ iEdg ⁡ G = A
16 4 fveq1d ⊢ φ → iEdg ⁡ G ⁡ i = A N ⁡ i
17 16 eleq2d ⊢ φ → K ∈ iEdg ⁡ G ⁡ i ↔ K ∈ A N ⁡ i
18 15 17 rexeqbidv ⊢ φ → ∃ i ∈ dom ⁡ iEdg ⁡ G K ∈ iEdg ⁡ G ⁡ i ↔ ∃ i ∈ A K ∈ A N ⁡ i
19 fveq2 ⊢ i = A → A N ⁡ i = A N ⁡ A
20 19 eleq2d ⊢ i = A → K ∈ A N ⁡ i ↔ K ∈ A N ⁡ A
21 20 rexsng ⊢ A ∈ X → ∃ i ∈ A K ∈ A N ⁡ i ↔ K ∈ A N ⁡ A
22 2 21 syl ⊢ φ → ∃ i ∈ A K ∈ A N ⁡ i ↔ K ∈ A N ⁡ A
23 18 22 bitrd ⊢ φ → ∃ i ∈ dom ⁡ iEdg ⁡ G K ∈ iEdg ⁡ G ⁡ i ↔ K ∈ A N ⁡ A
24 11 23 mtbird ⊢ φ → ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G K ∈ iEdg ⁡ G ⁡ i
25 5 eldifad ⊢ φ → K ∈ V
26 1 eleq2d ⊢ φ → K ∈ Vtx ⁡ G ↔ K ∈ V
27 25 26 mpbird ⊢ φ → K ∈ Vtx ⁡ G
28 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
29 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
30 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
31 28 29 30 vtxd0nedgb ⊢ K ∈ Vtx ⁡ G → VtxDeg ⁡ G ⁡ K = 0 ↔ ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G K ∈ iEdg ⁡ G ⁡ i
32 27 31 syl ⊢ φ → VtxDeg ⁡ G ⁡ K = 0 ↔ ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G K ∈ iEdg ⁡ G ⁡ i
33 24 32 mpbird ⊢ φ → VtxDeg ⁡ G ⁡ K = 0