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 ⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion umgr2v2evd2 ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐴 ) = 2 )

Proof

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