Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uspgrloopvd2 Structured version   Visualization version   Unicode version

Theorem uspgrloopvd2 39606
Description: In a simple pseudograph with one edge which is a loop (see uspgr1v1eop 39373), the vertex connected with itself by the loop has degree 2. (Contributed by AV, 17-Dec-2020.)
Hypothesis
Ref Expression
uspgrloopvtx.g  |-  G  = 
<. V ,  { <. 0 ,  { A } >. } >.
Assertion
Ref Expression
uspgrloopvd2  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( (VtxDeg `  G
) `  A )  =  2 )

Proof of Theorem uspgrloopvd2
Dummy variables  a 
e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 c0ex 9662 . . . . 5  |-  0  e.  _V
2 uspgrloopvtx.g . . . . . 6  |-  G  = 
<. V ,  { <. 0 ,  { A } >. } >.
3 uspgr1v1eop 39373 . . . . . 6  |-  ( ( V  e.  W  /\  0  e.  _V  /\  A  e.  V )  ->  <. V ,  { <. 0 ,  { A } >. } >.  e. USPGraph  )
42, 3syl5eqel 2543 . . . . 5  |-  ( ( V  e.  W  /\  0  e.  _V  /\  A  e.  V )  ->  G  e. USPGraph  )
51, 4mp3an2 1361 . . . 4  |-  ( ( V  e.  W  /\  A  e.  V )  ->  G  e. USPGraph  )
6 uspgrushgr 39309 . . . 4  |-  ( G  e. USPGraph  ->  G  e. USHGraph  )
75, 6syl 17 . . 3  |-  ( ( V  e.  W  /\  A  e.  V )  ->  G  e. USHGraph  )
82uspgrloopvtxel 39603 . . 3  |-  ( ( V  e.  W  /\  A  e.  V )  ->  A  e.  (Vtx `  G ) )
9 eqid 2461 . . . 4  |-  (Vtx `  G )  =  (Vtx
`  G )
10 eqid 2461 . . . 4  |-  (Edg `  G )  =  (Edg
`  G )
11 eqid 2461 . . . 4  |-  (VtxDeg `  G )  =  (VtxDeg `  G )
129, 10, 11vtxdushgrfvedg 39592 . . 3  |-  ( ( G  e. USHGraph  /\  A  e.  (Vtx `  G )
)  ->  ( (VtxDeg `  G ) `  A
)  =  ( (
# `  { e  e.  (Edg `  G )  |  A  e.  e } ) +e
( # `  { e  e.  (Edg `  G
)  |  e  =  { A } }
) ) )
137, 8, 12syl2anc 671 . 2  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( (VtxDeg `  G
) `  A )  =  ( ( # `  { e  e.  (Edg
`  G )  |  A  e.  e } ) +e (
# `  { e  e.  (Edg `  G )  |  e  =  { A } } ) ) )
14 eqid 2461 . . . . . . . 8  |-  { { A } }  =  { { A } }
15 snex 4654 . . . . . . . . 9  |-  { A }  e.  _V
16 sneq 3989 . . . . . . . . . 10  |-  ( a  =  { A }  ->  { a }  =  { { A } }
)
1716eqeq2d 2471 . . . . . . . . 9  |-  ( a  =  { A }  ->  ( { { A } }  =  {
a }  <->  { { A } }  =  { { A } } ) )
1815, 17spcev 3152 . . . . . . . 8  |-  ( { { A } }  =  { { A } }  ->  E. a { { A } }  =  {
a } )
1914, 18ax-mp 5 . . . . . . 7  |-  E. a { { A } }  =  { a }
2019a1i 11 . . . . . 6  |-  ( ( V  e.  W  /\  A  e.  V )  ->  E. a { { A } }  =  {
a } )
21 snidg 4005 . . . . . . . . . 10  |-  ( A  e.  V  ->  A  e.  { A } )
2221adantl 472 . . . . . . . . 9  |-  ( ( V  e.  W  /\  A  e.  V )  ->  A  e.  { A } )
2322iftrued 3900 . . . . . . . 8  |-  ( ( V  e.  W  /\  A  e.  V )  ->  if ( A  e. 
{ A } ,  { { A } } ,  (/) )  =  { { A } } )
2423eqeq1d 2463 . . . . . . 7  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( if ( A  e.  { A } ,  { { A } } ,  (/) )  =  { a }  <->  { { A } }  =  {
a } ) )
2524exbidv 1778 . . . . . 6  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( E. a if ( A  e.  { A } ,  { { A } } ,  (/) )  =  { a } 
<->  E. a { { A } }  =  {
a } ) )
2620, 25mpbird 240 . . . . 5  |-  ( ( V  e.  W  /\  A  e.  V )  ->  E. a if ( A  e.  { A } ,  { { A } } ,  (/) )  =  { a } )
272uspgrloopedg 39604 . . . . . . . . 9  |-  ( ( V  e.  W  /\  A  e.  V )  ->  (Edg `  G )  =  { { A } } )
2827rabeqdv 3050 . . . . . . . 8  |-  ( ( V  e.  W  /\  A  e.  V )  ->  { e  e.  (Edg
`  G )  |  A  e.  e }  =  { e  e. 
{ { A } }  |  A  e.  e } )
29 eleq2 2528 . . . . . . . . 9  |-  ( e  =  { A }  ->  ( A  e.  e  <-> 
A  e.  { A } ) )
3029rabsnif 4053 . . . . . . . 8  |-  { e  e.  { { A } }  |  A  e.  e }  =  if ( A  e.  { A } ,  { { A } } ,  (/) )
3128, 30syl6eq 2511 . . . . . . 7  |-  ( ( V  e.  W  /\  A  e.  V )  ->  { e  e.  (Edg
`  G )  |  A  e.  e }  =  if ( A  e.  { A } ,  { { A } } ,  (/) ) )
3231eqeq1d 2463 . . . . . 6  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( { e  e.  (Edg `  G )  |  A  e.  e }  =  { a } 
<->  if ( A  e. 
{ A } ,  { { A } } ,  (/) )  =  {
a } ) )
3332exbidv 1778 . . . . 5  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( E. a { e  e.  (Edg `  G )  |  A  e.  e }  =  {
a }  <->  E. a if ( A  e.  { A } ,  { { A } } ,  (/) )  =  { a } ) )
3426, 33mpbird 240 . . . 4  |-  ( ( V  e.  W  /\  A  e.  V )  ->  E. a { e  e.  (Edg `  G
)  |  A  e.  e }  =  {
a } )
35 fvex 5897 . . . . . 6  |-  (Edg `  G )  e.  _V
3635rabex 4567 . . . . 5  |-  { e  e.  (Edg `  G
)  |  A  e.  e }  e.  _V
37 hash1snb 12625 . . . . 5  |-  ( { e  e.  (Edg `  G )  |  A  e.  e }  e.  _V  ->  ( ( # `  {
e  e.  (Edg `  G )  |  A  e.  e } )  =  1  <->  E. a { e  e.  (Edg `  G
)  |  A  e.  e }  =  {
a } ) )
3836, 37ax-mp 5 . . . 4  |-  ( (
# `  { e  e.  (Edg `  G )  |  A  e.  e } )  =  1  <->  E. a { e  e.  (Edg `  G )  |  A  e.  e }  =  { a } )
3934, 38sylibr 217 . . 3  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( # `  {
e  e.  (Edg `  G )  |  A  e.  e } )  =  1 )
40 eqid 2461 . . . . . . . . 9  |-  { A }  =  { A }
4140iftruei 3899 . . . . . . . 8  |-  if ( { A }  =  { A } ,  { { A } } ,  (/) )  =  { { A } }
4241eqeq1i 2466 . . . . . . 7  |-  ( if ( { A }  =  { A } ,  { { A } } ,  (/) )  =  {
a }  <->  { { A } }  =  {
a } )
4342exbii 1728 . . . . . 6  |-  ( E. a if ( { A }  =  { A } ,  { { A } } ,  (/) )  =  { a } 
<->  E. a { { A } }  =  {
a } )
4420, 43sylibr 217 . . . . 5  |-  ( ( V  e.  W  /\  A  e.  V )  ->  E. a if ( { A }  =  { A } ,  { { A } } ,  (/) )  =  { a } )
4527rabeqdv 3050 . . . . . . . 8  |-  ( ( V  e.  W  /\  A  e.  V )  ->  { e  e.  (Edg
`  G )  |  e  =  { A } }  =  {
e  e.  { { A } }  |  e  =  { A } } )
46 eqeq1 2465 . . . . . . . . 9  |-  ( e  =  { A }  ->  ( e  =  { A }  <->  { A }  =  { A } ) )
4746rabsnif 4053 . . . . . . . 8  |-  { e  e.  { { A } }  |  e  =  { A } }  =  if ( { A }  =  { A } ,  { { A } } ,  (/) )
4845, 47syl6eq 2511 . . . . . . 7  |-  ( ( V  e.  W  /\  A  e.  V )  ->  { e  e.  (Edg
`  G )  |  e  =  { A } }  =  if ( { A }  =  { A } ,  { { A } } ,  (/) ) )
4948eqeq1d 2463 . . . . . 6  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( { e  e.  (Edg `  G )  |  e  =  { A } }  =  {
a }  <->  if ( { A }  =  { A } ,  { { A } } ,  (/) )  =  { a } ) )
5049exbidv 1778 . . . . 5  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( E. a { e  e.  (Edg `  G )  |  e  =  { A } }  =  { a } 
<->  E. a if ( { A }  =  { A } ,  { { A } } ,  (/) )  =  { a } ) )
5144, 50mpbird 240 . . . 4  |-  ( ( V  e.  W  /\  A  e.  V )  ->  E. a { e  e.  (Edg `  G
)  |  e  =  { A } }  =  { a } )
5235rabex 4567 . . . . 5  |-  { e  e.  (Edg `  G
)  |  e  =  { A } }  e.  _V
53 hash1snb 12625 . . . . 5  |-  ( { e  e.  (Edg `  G )  |  e  =  { A } }  e.  _V  ->  ( ( # `  {
e  e.  (Edg `  G )  |  e  =  { A } } )  =  1  <->  E. a { e  e.  (Edg `  G )  |  e  =  { A } }  =  {
a } ) )
5452, 53ax-mp 5 . . . 4  |-  ( (
# `  { e  e.  (Edg `  G )  |  e  =  { A } } )  =  1  <->  E. a { e  e.  (Edg `  G
)  |  e  =  { A } }  =  { a } )
5551, 54sylibr 217 . . 3  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( # `  {
e  e.  (Edg `  G )  |  e  =  { A } } )  =  1 )
5639, 55oveq12d 6332 . 2  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( ( # `  {
e  e.  (Edg `  G )  |  A  e.  e } ) +e ( # `  {
e  e.  (Edg `  G )  |  e  =  { A } } ) )  =  ( 1 +e 1 ) )
57 1re 9667 . . . . 5  |-  1  e.  RR
58 rexadd 11553 . . . . 5  |-  ( ( 1  e.  RR  /\  1  e.  RR )  ->  ( 1 +e 1 )  =  ( 1  +  1 ) )
5957, 57, 58mp2an 683 . . . 4  |-  ( 1 +e 1 )  =  ( 1  +  1 )
60 1p1e2 10750 . . . 4  |-  ( 1  +  1 )  =  2
6159, 60eqtri 2483 . . 3  |-  ( 1 +e 1 )  =  2
6261a1i 11 . 2  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( 1 +e 1 )  =  2 )
6313, 56, 623eqtrd 2499 1  |-  ( ( V  e.  W  /\  A  e.  V )  ->  ( (VtxDeg `  G
) `  A )  =  2 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1454   E.wex 1673    e. wcel 1897   {crab 2752   _Vcvv 3056   (/)c0 3742   ifcif 3892   {csn 3979   <.cop 3985   ` cfv 5600  (class class class)co 6314   RRcr 9563   0cc0 9564   1c1 9565    + caddc 9567   2c2 10686   +ecxad 11435   #chash 12546  Vtxcvtx 39146   USHGraph cushgr 39193  Edgcedga 39257   USPGraph cuspgr 39282  VtxDegcvtxdg 39575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-2 10695  df-n0 10898  df-z 10966  df-uz 11188  df-xadd 11438  df-fz 11813  df-hash 12547  df-vtx 39148  df-iedg 39149  df-uhgr 39194  df-ushgr 39195  df-edga 39258  df-uspgr 39284  df-vtxdg 39576
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator