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 e. W /\ A e. V /\ B e. 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 e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> G e. UMGraph )
3 1 umgr2v2evtxel 
 |-  ( ( V e. W /\ A e. V ) -> A e. ( Vtx ` G ) )
4 3 3adant3 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> A e. ( Vtx ` G ) )
5 4 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> A e. ( 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 e. UMGraph /\ A e. ( Vtx ` G ) ) -> ( ( VtxDeg ` G ) ` A ) = ( # ` { x e. dom ( iEdg ` G ) | A e. ( ( iEdg ` G ) ` x ) } ) )
11 2 5 10 syl2anc 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( ( VtxDeg ` G ) ` A ) = ( # ` { x e. dom ( iEdg ` G ) | A e. ( ( iEdg ` G ) ` x ) } ) )
12 1 umgr2v2eiedg 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( iEdg ` G ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
13 12 dmeqd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> dom ( iEdg ` G ) = dom { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
14 prex 
 |-  { A , B } e. _V
15 14 14 dmprop 
 |-  dom { <. 0 , { A , B } >. , <. 1 , { A , B } >. } = { 0 , 1 }
16 13 15 eqtrdi 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> dom ( iEdg ` G ) = { 0 , 1 } )
17 12 fveq1d 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( ( iEdg ` G ) ` x ) = ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) )
18 17 eleq2d 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( A e. ( ( iEdg ` G ) ` x ) <-> A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) ) )
19 16 18 rabeqbidv 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> { x e. dom ( iEdg ` G ) | A e. ( ( iEdg ` G ) ` x ) } = { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } )
20 19 fveq2d 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( # ` { x e. dom ( iEdg ` G ) | A e. ( ( iEdg ` G ) ` x ) } ) = ( # ` { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } ) )
21 prid1g 
 |-  ( A e. V -> A e. { A , B } )
22 0ne1 
 |-  0 =/= 1
23 c0ex 
 |-  0 e. _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 e. V -> A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` 0 ) )
27 1ex 
 |-  1 e. _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 e. V -> A e. ( { <. 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 e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) <-> A e. ( { <. 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 e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) <-> A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` 1 ) ) )
35 23 27 32 34 ralpr 
 |-  ( A. x e. { 0 , 1 } A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) <-> ( A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` 0 ) /\ A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` 1 ) ) )
36 26 30 35 sylanbrc 
 |-  ( A e. V -> A. x e. { 0 , 1 } A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) )
37 rabid2 
 |-  ( { 0 , 1 } = { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } <-> A. x e. { 0 , 1 } A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) )
38 36 37 sylibr 
 |-  ( A e. V -> { 0 , 1 } = { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } )
39 38 eqcomd 
 |-  ( A e. V -> { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } = { 0 , 1 } )
40 39 fveq2d 
 |-  ( A e. V -> ( # ` { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } ) = ( # ` { 0 , 1 } ) )
41 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
42 40 41 eqtrdi 
 |-  ( A e. V -> ( # ` { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } ) = 2 )
43 42 3ad2ant2 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( # ` { x e. { 0 , 1 } | A e. ( { <. 0 , { A , B } >. , <. 1 , { A , B } >. } ` x ) } ) = 2 )
44 20 43 eqtrd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( # ` { x e. dom ( iEdg ` G ) | A e. ( ( iEdg ` G ) ` x ) } ) = 2 )
45 44 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` { x e. dom ( iEdg ` G ) | A e. ( ( iEdg ` G ) ` x ) } ) = 2 )
46 11 45 eqtrd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( ( VtxDeg ` G ) ` A ) = 2 )