Metamath Proof Explorer

Theorem umgr2v2evd2

Description: In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g ⊢ G = V 0 A B 1 A B
Assertion umgr2v2evd2 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → VtxDeg ⁡ G ⁡ A = 2

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢ G = V 0 A B 1 A B
2 1 umgr2v2e ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → G ∈ UMGraph
3 1 umgr2v2evtxel ⊢ V ∈ W ∧ A ∈ V → A ∈ Vtx ⁡ G
4 3 3adant3 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → A ∈ Vtx ⁡ G
5 4 adantr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ∈ Vtx ⁡ G
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
8 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
9 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
10 6 7 8 9 vtxdumgrval ⊢ G ∈ UMGraph ∧ A ∈ Vtx ⁡ G → VtxDeg ⁡ G ⁡ A = x ∈ dom ⁡ iEdg ⁡ G | A ∈ iEdg ⁡ G ⁡ x
11 2 5 10 syl2anc ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → VtxDeg ⁡ G ⁡ A = x ∈ dom ⁡ iEdg ⁡ G | A ∈ iEdg ⁡ G ⁡ x
12 1 umgr2v2eiedg ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → iEdg ⁡ G = 0 A B 1 A B
13 12 dmeqd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → dom ⁡ iEdg ⁡ G = dom ⁡ 0 A B 1 A B
14 prex ⊢ A B ∈ V
15 14 14 dmprop ⊢ dom ⁡ 0 A B 1 A B = 0 1
16 13 15 eqtrdi ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → dom ⁡ iEdg ⁡ G = 0 1
17 12 fveq1d ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → iEdg ⁡ G ⁡ x = 0 A B 1 A B ⁡ x
18 17 eleq2d ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → A ∈ iEdg ⁡ G ⁡ x ↔ A ∈ 0 A B 1 A B ⁡ x
19 16 18 rabeqbidv ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → x ∈ dom ⁡ iEdg ⁡ G | A ∈ iEdg ⁡ G ⁡ x = x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x
20 19 fveq2d ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → x ∈ dom ⁡ iEdg ⁡ G | A ∈ iEdg ⁡ G ⁡ x = x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x
21 prid1g ⊢ A ∈ V → A ∈ A B
22 0ne1 ⊢ 0 ≠ 1
23 c0ex ⊢ 0 ∈ V
24 23 14 fvpr1 ⊢ 0 ≠ 1 → 0 A B 1 A B ⁡ 0 = A B
25 22 24 ax-mp ⊢ 0 A B 1 A B ⁡ 0 = A B
26 21 25 eleqtrrdi ⊢ A ∈ V → A ∈ 0 A B 1 A B ⁡ 0
27 1ex ⊢ 1 ∈ V
28 27 14 fvpr2 ⊢ 0 ≠ 1 → 0 A B 1 A B ⁡ 1 = A B
29 22 28 ax-mp ⊢ 0 A B 1 A B ⁡ 1 = A B
30 21 29 eleqtrrdi ⊢ A ∈ V → A ∈ 0 A B 1 A B ⁡ 1
31 fveq2 ⊢ x = 0 → 0 A B 1 A B ⁡ x = 0 A B 1 A B ⁡ 0
32 31 eleq2d ⊢ x = 0 → A ∈ 0 A B 1 A B ⁡ x ↔ A ∈ 0 A B 1 A B ⁡ 0
33 fveq2 ⊢ x = 1 → 0 A B 1 A B ⁡ x = 0 A B 1 A B ⁡ 1
34 33 eleq2d ⊢ x = 1 → A ∈ 0 A B 1 A B ⁡ x ↔ A ∈ 0 A B 1 A B ⁡ 1
35 23 27 32 34 ralpr ⊢ ∀ x ∈ 0 1 A ∈ 0 A B 1 A B ⁡ x ↔ A ∈ 0 A B 1 A B ⁡ 0 ∧ A ∈ 0 A B 1 A B ⁡ 1
36 26 30 35 sylanbrc ⊢ A ∈ V → ∀ x ∈ 0 1 A ∈ 0 A B 1 A B ⁡ x
37 rabid2 ⊢ 0 1 = x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x ↔ ∀ x ∈ 0 1 A ∈ 0 A B 1 A B ⁡ x
38 36 37 sylibr ⊢ A ∈ V → 0 1 = x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x
39 38 eqcomd ⊢ A ∈ V → x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x = 0 1
40 39 fveq2d ⊢ A ∈ V → x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x = 0 1
41 prhash2ex ⊢ 0 1 = 2
42 40 41 eqtrdi ⊢ A ∈ V → x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x = 2
43 42 3ad2ant2 ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → x ∈ 0 1 | A ∈ 0 A B 1 A B ⁡ x = 2
44 20 43 eqtrd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → x ∈ dom ⁡ iEdg ⁡ G | A ∈ iEdg ⁡ G ⁡ x = 2
45 44 adantr ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → x ∈ dom ⁡ iEdg ⁡ G | A ∈ iEdg ⁡ G ⁡ x = 2
46 11 45 eqtrd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → VtxDeg ⁡ G ⁡ A = 2