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 )