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

Theorem usgfis 40031
Description: An undirected simple graph of finite order (i.e. with a finite number of vertices) is of finite size, i.e. it has also only a finite number of edges, analogous to usgrafis 25192. Remark: The proof of this theorem is very long compared with usgrafis 25192, because the theorem brfi1ind 12685 to perform the finite induction is taylored for binary relations, so that the theorem itself and the used lemmas must be transformed accordingly. Maybe a variant of brfi1ind 12685 could be provided, which is better suitable for this theorem. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 11-Jan-2018.) (Proof modification is discouraged.)
Assertion
Ref Expression
usgfis  |-  ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 )

Proof of Theorem usgfis
Dummy variables  e 
f  v  w  y  p  q  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fusgraimpcl 40012 . 2  |-  ( G  e. FinUSGrph  ->  ( G  e. USGrph  /\  ( GrOrder  `  G )  e.  NN0 ) )
2 relusgra 25111 . . . . . . . . . . 11  |-  Rel USGrph
3 1st2nd 6866 . . . . . . . . . . 11  |-  ( ( Rel USGrph  /\  G  e. USGrph  )  ->  G  =  <. ( 1st `  G ) ,  ( 2nd `  G
) >. )
42, 3mpan 681 . . . . . . . . . 10  |-  ( G  e. USGrph  ->  G  =  <. ( 1st `  G ) ,  ( 2nd `  G
) >. )
5 eleq1 2528 . . . . . . . . . . . 12  |-  ( G  =  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  ->  ( G  e. USGrph  <->  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  e. USGrph  )
)
6 df-br 4417 . . . . . . . . . . . 12  |-  ( ( 1st `  G ) USGrph 
( 2nd `  G
)  <->  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  e. USGrph  )
75, 6syl6bbr 271 . . . . . . . . . . 11  |-  ( G  =  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  ->  ( G  e. USGrph  <->  ( 1st `  G
) USGrph  ( 2nd `  G
) ) )
8 mptresid 5178 . . . . . . . . . . . . . 14  |-  ( q  e.  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  |->  q )  =  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e
>. )  |  n  e/  p } )
9 fvex 5898 . . . . . . . . . . . . . . 15  |-  ( Edges  `  <. v ,  e >. )  e.  _V
109mptrabex 6162 . . . . . . . . . . . . . 14  |-  ( q  e.  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  |->  q )  e.  _V
118, 10eqeltrri 2537 . . . . . . . . . . . . 13  |-  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e
>. )  |  n  e/  p } )  e. 
_V
12 eleq1 2528 . . . . . . . . . . . . . 14  |-  ( e  =  ( 2nd `  G
)  ->  ( e  e.  Fin  <->  ( 2nd `  G
)  e.  Fin )
)
1312adantl 472 . . . . . . . . . . . . 13  |-  ( ( v  =  ( 1st `  G )  /\  e  =  ( 2nd `  G
) )  ->  (
e  e.  Fin  <->  ( 2nd `  G )  e.  Fin ) )
14 eleq1 2528 . . . . . . . . . . . . . 14  |-  ( e  =  f  ->  (
e  e.  Fin  <->  f  e.  Fin ) )
1514adantl 472 . . . . . . . . . . . . 13  |-  ( ( v  =  w  /\  e  =  f )  ->  ( e  e.  Fin  <->  f  e.  Fin ) )
16 df-br 4417 . . . . . . . . . . . . . 14  |-  ( v USGrph 
e  <->  <. v ,  e
>.  e. USGrph  )
17 opex 4678 . . . . . . . . . . . . . . . . 17  |-  <. v ,  e >.  e.  _V
18 vtxvalaltv 39968 . . . . . . . . . . . . . . . . 17  |-  ( <.
v ,  e >.  e.  _V  ->  ( VtxALTV  `  <. v ,  e >. )  =  ( 1st `  <. v ,  e >. )
)
1917, 18ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( VtxALTV  `  <. v ,  e >. )  =  ( 1st `  <. v ,  e >. )
20 vex 3060 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
21 vex 3060 . . . . . . . . . . . . . . . . 17  |-  e  e. 
_V
2220, 21op1st 6828 . . . . . . . . . . . . . . . 16  |-  ( 1st `  <. v ,  e
>. )  =  v
2319, 22eqtr2i 2485 . . . . . . . . . . . . . . 15  |-  v  =  ( VtxALTV  `  <. v ,  e >. )
24 eqid 2462 . . . . . . . . . . . . . . 15  |-  ( Edges  `  <. v ,  e >. )  =  ( Edges  `  <. v ,  e >. )
25 eqid 2462 . . . . . . . . . . . . . . 15  |-  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  =  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }
2623, 24, 25usgresvm1 40028 . . . . . . . . . . . . . 14  |-  ( (
<. v ,  e >.  e. USGrph  /\  n  e.  v )  ->  ( v  \  { n } ) USGrph 
(  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } ) )
2716, 26sylanb 479 . . . . . . . . . . . . 13  |-  ( ( v USGrph  e  /\  n  e.  v )  ->  (
v  \  { n } ) USGrph  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } ) )
28 eleq1 2528 . . . . . . . . . . . . . 14  |-  ( f  =  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  ->  (
f  e.  Fin  <->  (  _I  |` 
{ p  e.  ( Edges  `  <. v ,  e
>. )  |  n  e/  p } )  e. 
Fin ) )
2928adantl 472 . . . . . . . . . . . . 13  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } ) )  -> 
( f  e.  Fin  <->  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin ) )
30 usgrafisbaseALT 40025 . . . . . . . . . . . . 13  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  0 )  ->  e  e.  Fin )
31 residfi 39081 . . . . . . . . . . . . . . . 16  |-  ( (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin  <->  {
p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  e.  Fin )
32 simpr1 1020 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
v USGrph  e )
33 eleq1 2528 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  +  1 )  =  ( # `  v
)  ->  ( (
y  +  1 )  e.  NN0  <->  ( # `  v
)  e.  NN0 )
)
3433eqcoms 2470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  v )  =  ( y  +  1 )  ->  (
( y  +  1 )  e.  NN0  <->  ( # `  v
)  e.  NN0 )
)
35 hashclb 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  e.  _V  ->  (
v  e.  Fin  <->  ( # `  v
)  e.  NN0 )
)
3635bicomd 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  e.  _V  ->  (
( # `  v )  e.  NN0  <->  v  e.  Fin ) )
3720, 36ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  v )  e.  NN0  <->  v  e.  Fin )
3837biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  v )  e.  NN0  ->  v  e.  Fin )
3934, 38syl6bi 236 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  v )  =  ( y  +  1 )  ->  (
( y  +  1 )  e.  NN0  ->  v  e.  Fin ) )
40393ad2ant2 1036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  (
( y  +  1 )  e.  NN0  ->  v  e.  Fin ) )
4140impcom 436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
v  e.  Fin )
4232, 41jca 539 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( v USGrph  e  /\  v  e.  Fin )
)
43 usgrav 25114 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v USGrph 
e  ->  ( v  e.  _V  /\  e  e. 
_V ) )
44 df-br 4417 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v FinUSGrph  e 
<-> 
<. v ,  e >.  e. FinUSGrph  )
45 isfusgra0 40010 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  _V  /\  e  e.  _V )  ->  ( v FinUSGrph  e  <->  ( v USGrph  e  /\  v  e.  Fin ) ) )
4644, 45syl5bbr 267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  _V  /\  e  e.  _V )  ->  ( <. v ,  e
>.  e. FinUSGrph 
<->  ( v USGrph  e  /\  v  e.  Fin )
) )
4743, 46syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v USGrph 
e  ->  ( <. v ,  e >.  e. FinUSGrph  <->  ( v USGrph  e  /\  v  e.  Fin ) ) )
48473ad2ant1 1035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  ( <. v ,  e >.  e. FinUSGrph  <->  ( v USGrph  e  /\  v  e.  Fin ) ) )
4948adantl 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( <. v ,  e
>.  e. FinUSGrph 
<->  ( v USGrph  e  /\  v  e.  Fin )
) )
5042, 49mpbird 240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  ->  <. v ,  e >.  e. FinUSGrph  )
5117, 18mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v USGrph 
e  ->  ( VtxALTV  `  <. v ,  e >. )  =  ( 1st `  <. v ,  e >. )
)
5251, 22syl6req 2513 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v USGrph 
e  ->  v  =  ( VtxALTV  `  <. v ,  e
>. ) )
5352eleq2d 2525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v USGrph 
e  ->  ( n  e.  v  <->  n  e.  ( VtxALTV  ` 
<. v ,  e >.
) ) )
5453biimpd 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v USGrph 
e  ->  ( n  e.  v  ->  n  e.  ( VtxALTV  `  <. v ,  e >. ) ) )
5554a1d 26 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v USGrph 
e  ->  ( ( # `
 v )  =  ( y  +  1 )  ->  ( n  e.  v  ->  n  e.  ( VtxALTV  `  <. v ,  e >. ) ) ) )
56553imp 1208 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  n  e.  ( VtxALTV  `  <. v ,  e >. )
)
5756adantl 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  ->  n  e.  ( VtxALTV  `  <. v ,  e >. )
)
5850, 57jca 539 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( <. v ,  e
>.  e. FinUSGrph  /\  n  e.  ( VtxALTV  `  <. v ,  e
>. ) ) )
59 eqid 2462 . . . . . . . . . . . . . . . . . . 19  |-  ( VtxALTV  `  <. v ,  e >. )  =  ( VtxALTV  `  <. v ,  e >. )
60 df-ov 6318 . . . . . . . . . . . . . . . . . . 19  |-  ( v Edges 
e )  =  ( Edges  `  <. v ,  e
>. )
6160eqcomi 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( Edges  `  <. v ,  e >. )  =  ( v Edges  e
)
62 rabeq 3050 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Edges  `  <. v ,  e
>. )  =  (
v Edges  e )  ->  { p  e.  ( Edges  ` 
<. v ,  e >.
)  |  n  e/  p }  =  {
p  e.  ( v Edges 
e )  |  n  e/  p } )
6361, 62ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  =  { p  e.  ( v Edges  e )  |  n  e/  p }
6459, 60, 63usgfislem2 40030 . . . . . . . . . . . . . . . . . 18  |-  ( (
<. v ,  e >.  e. FinUSGrph 
/\  n  e.  ( VtxALTV  `  <. v ,  e
>. ) )  ->  (
( v Edges  e )  e.  Fin  <->  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  e.  Fin )
)
6558, 64syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( ( v Edges  e
)  e.  Fin  <->  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  e.  Fin )
)
6665biimprd 231 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  e.  Fin  ->  ( v Edges  e
)  e.  Fin )
)
6731, 66syl5bi 225 . . . . . . . . . . . . . . 15  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin  ->  ( v Edges  e )  e.  Fin ) )
6867imp 435 . . . . . . . . . . . . . 14  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `  v )  =  ( y  +  1 )  /\  n  e.  v ) )  /\  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin )  ->  ( v Edges  e
)  e.  Fin )
69 usgedgffibi 40019 . . . . . . . . . . . . . . . . 17  |-  ( v USGrph 
e  ->  ( e  e.  Fin  <->  ( v Edges  e
)  e.  Fin )
)
70693ad2ant1 1035 . . . . . . . . . . . . . . . 16  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  (
e  e.  Fin  <->  ( v Edges  e )  e.  Fin ) )
7170adantl 472 . . . . . . . . . . . . . . 15  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( e  e.  Fin  <->  (
v Edges  e )  e. 
Fin ) )
7271adantr 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `  v )  =  ( y  +  1 )  /\  n  e.  v ) )  /\  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin )  ->  ( e  e. 
Fin 
<->  ( v Edges  e )  e.  Fin ) )
7368, 72mpbird 240 . . . . . . . . . . . . 13  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `  v )  =  ( y  +  1 )  /\  n  e.  v ) )  /\  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin )  ->  e  e.  Fin )
742, 11, 13, 15, 27, 29, 30, 73brfi1ind 12685 . . . . . . . . . . . 12  |-  ( ( ( 1st `  G
) USGrph  ( 2nd `  G
)  /\  ( 1st `  G )  e.  Fin )  ->  ( 2nd `  G
)  e.  Fin )
7574ex 440 . . . . . . . . . . 11  |-  ( ( 1st `  G ) USGrph 
( 2nd `  G
)  ->  ( ( 1st `  G )  e. 
Fin  ->  ( 2nd `  G
)  e.  Fin )
)
767, 75syl6bi 236 . . . . . . . . . 10  |-  ( G  =  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  ->  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( 2nd `  G )  e. 
Fin ) ) )
774, 76mpcom 37 . . . . . . . . 9  |-  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( 2nd `  G
)  e.  Fin )
)
7877imp 435 . . . . . . . 8  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  ( 2nd `  G )  e. 
Fin )
79 rnfi 7883 . . . . . . . 8  |-  ( ( 2nd `  G )  e.  Fin  ->  ran  ( 2nd `  G )  e.  Fin )
8078, 79syl 17 . . . . . . 7  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  ran  ( 2nd `  G )  e.  Fin )
81 edgval 25115 . . . . . . . . 9  |-  ( G  e. USGrph  ->  ( Edges  `  G )  =  ran  ( 2nd `  G ) )
8281eleq1d 2524 . . . . . . . 8  |-  ( G  e. USGrph  ->  ( ( Edges  `  G
)  e.  Fin  <->  ran  ( 2nd `  G )  e.  Fin ) )
8382adantr 471 . . . . . . 7  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  (
( Edges  `  G )  e. 
Fin 
<->  ran  ( 2nd `  G
)  e.  Fin )
)
8480, 83mpbird 240 . . . . . 6  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  ( Edges  `  G )  e.  Fin )
8584ex 440 . . . . 5  |-  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( Edges  `  G )  e.  Fin ) )
8685a1dd 47 . . . 4  |-  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( G  e. FinUSGrph  ->  ( Edges  `  G )  e.  Fin ) ) )
87 gordval 39973 . . . . . 6  |-  ( G  e. USGrph  ->  ( GrOrder  `  G )  =  ( # `  ( 1st `  G ) ) )
8887eleq1d 2524 . . . . 5  |-  ( G  e. USGrph  ->  ( ( GrOrder  `  G
)  e.  NN0  <->  ( # `  ( 1st `  G ) )  e.  NN0 ) )
89 fvex 5898 . . . . . 6  |-  ( 1st `  G )  e.  _V
90 hashclb 12572 . . . . . 6  |-  ( ( 1st `  G )  e.  _V  ->  (
( 1st `  G
)  e.  Fin  <->  ( # `  ( 1st `  G ) )  e.  NN0 ) )
9189, 90ax-mp 5 . . . . 5  |-  ( ( 1st `  G )  e.  Fin  <->  ( # `  ( 1st `  G ) )  e.  NN0 )
9288, 91syl6bbr 271 . . . 4  |-  ( G  e. USGrph  ->  ( ( GrOrder  `  G
)  e.  NN0  <->  ( 1st `  G )  e.  Fin ) )
93 usgsizedg 39980 . . . . . . 7  |-  ( G  e. USGrph  ->  ( GrSize  `  G )  =  ( # `  ( Edges  `  G ) ) )
9493eleq1d 2524 . . . . . 6  |-  ( G  e. USGrph  ->  ( ( GrSize  `  G
)  e.  NN0  <->  ( # `  ( Edges  `  G ) )  e. 
NN0 ) )
95 fvex 5898 . . . . . . 7  |-  ( Edges  `  G
)  e.  _V
96 hashclb 12572 . . . . . . 7  |-  ( ( Edges  `  G )  e.  _V  ->  ( ( Edges  `  G
)  e.  Fin  <->  ( # `  ( Edges  `  G ) )  e. 
NN0 ) )
9795, 96ax-mp 5 . . . . . 6  |-  ( ( Edges  `  G )  e.  Fin  <->  ( # `
 ( Edges  `  G
) )  e.  NN0 )
9894, 97syl6bbr 271 . . . . 5  |-  ( G  e. USGrph  ->  ( ( GrSize  `  G
)  e.  NN0  <->  ( Edges  `  G
)  e.  Fin )
)
9998imbi2d 322 . . . 4  |-  ( G  e. USGrph  ->  ( ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 )  <->  ( G  e. FinUSGrph 
->  ( Edges  `  G )  e.  Fin ) ) )
10086, 92, 993imtr4d 276 . . 3  |-  ( G  e. USGrph  ->  ( ( GrOrder  `  G
)  e.  NN0  ->  ( G  e. FinUSGrph  ->  ( GrSize  `  G
)  e.  NN0 )
) )
101100imp 435 . 2  |-  ( ( G  e. USGrph  /\  ( GrOrder  `  G )  e.  NN0 )  ->  ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 ) )
1021, 101mpcom 37 1  |-  ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    e/ wnel 2634   {crab 2753   _Vcvv 3057    \ cdif 3413   {csn 3980   <.cop 3986   class class class wbr 4416    |-> cmpt 4475    _I cid 4763   ran crn 4854    |` cres 4855   Rel wrel 4858   ` cfv 5601  (class class class)co 6315   1stc1st 6818   2ndc2nd 6819   Fincfn 7595   1c1 9566    + caddc 9568   NN0cn0 10898   #chash 12547   USGrph cusg 25106   Edges cedg 25107   VtxALTV cvtxaltv 39966   GrOrder cgord 39969   GrSize cgsiz 39970   FinUSGrph cfusg 40006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-n0 10899  df-z 10967  df-uz 11189  df-fz 11814  df-hash 12548  df-uhgra 25068  df-umgra 25089  df-uslgra 25108  df-usgra 25109  df-edg 25112  df-vtxALTV 39967  df-gord 39971  df-gsiz 39972  df-fusg 40007
This theorem is referenced by:  usgrafiedgALT  40036
  Copyright terms: Public domain W3C validator