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

Theorem usgfis 32803
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 24561. Remark: The proof of this theorem is very long compared with usgrafis 24561, because the theorem brfi1ind 12460 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 12460 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 32784 . 2  |-  ( G  e. FinUSGrph  ->  ( G  e. USGrph  /\  ( GrOrder  `  G )  e.  NN0 ) )
2 relusgra 24481 . . . . . . . . . . 11  |-  Rel USGrph
3 1st2nd 6767 . . . . . . . . . . 11  |-  ( ( Rel USGrph  /\  G  e. USGrph  )  ->  G  =  <. ( 1st `  G ) ,  ( 2nd `  G
) >. )
42, 3mpan 668 . . . . . . . . . 10  |-  ( G  e. USGrph  ->  G  =  <. ( 1st `  G ) ,  ( 2nd `  G
) >. )
5 eleq1 2468 . . . . . . . . . . . 12  |-  ( G  =  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  ->  ( G  e. USGrph  <->  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  e. USGrph  )
)
6 df-br 4385 . . . . . . . . . . . 12  |-  ( ( 1st `  G ) USGrph 
( 2nd `  G
)  <->  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  e. USGrph  )
75, 6syl6bbr 263 . . . . . . . . . . 11  |-  ( G  =  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  ->  ( G  e. USGrph  <->  ( 1st `  G
) USGrph  ( 2nd `  G
) ) )
8 mptresid 5257 . . . . . . . . . . . . . 14  |-  ( q  e.  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  |->  q )  =  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e
>. )  |  n  e/  p } )
9 fvex 5801 . . . . . . . . . . . . . . 15  |-  ( Edges  `  <. v ,  e >. )  e.  _V
109mptrabex 6065 . . . . . . . . . . . . . 14  |-  ( q  e.  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  |->  q )  e.  _V
118, 10eqeltrri 2481 . . . . . . . . . . . . 13  |-  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e
>. )  |  n  e/  p } )  e. 
_V
12 eleq1 2468 . . . . . . . . . . . . . 14  |-  ( e  =  ( 2nd `  G
)  ->  ( e  e.  Fin  <->  ( 2nd `  G
)  e.  Fin )
)
1312adantl 464 . . . . . . . . . . . . 13  |-  ( ( v  =  ( 1st `  G )  /\  e  =  ( 2nd `  G
) )  ->  (
e  e.  Fin  <->  ( 2nd `  G )  e.  Fin ) )
14 eleq1 2468 . . . . . . . . . . . . . 14  |-  ( e  =  f  ->  (
e  e.  Fin  <->  f  e.  Fin ) )
1514adantl 464 . . . . . . . . . . . . 13  |-  ( ( v  =  w  /\  e  =  f )  ->  ( e  e.  Fin  <->  f  e.  Fin ) )
16 df-br 4385 . . . . . . . . . . . . . 14  |-  ( v USGrph 
e  <->  <. v ,  e
>.  e. USGrph  )
17 opex 4643 . . . . . . . . . . . . . . . . 17  |-  <. v ,  e >.  e.  _V
18 vtxval 32740 . . . . . . . . . . . . . . . . 17  |-  ( <.
v ,  e >.  e.  _V  ->  ( Vtx  `  <. v ,  e >. )  =  ( 1st `  <. v ,  e >. )
)
1917, 18ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( Vtx  `  <. v ,  e >.
)  =  ( 1st `  <. v ,  e
>. )
20 vex 3054 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
21 vex 3054 . . . . . . . . . . . . . . . . 17  |-  e  e. 
_V
2220, 21op1st 6729 . . . . . . . . . . . . . . . 16  |-  ( 1st `  <. v ,  e
>. )  =  v
2319, 22eqtr2i 2426 . . . . . . . . . . . . . . 15  |-  v  =  ( Vtx  `  <. v ,  e >. )
24 eqid 2396 . . . . . . . . . . . . . . 15  |-  ( Edges  `  <. v ,  e >. )  =  ( Edges  `  <. v ,  e >. )
25 eqid 2396 . . . . . . . . . . . . . . 15  |-  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  =  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }
2623, 24, 25usgresvm1 32800 . . . . . . . . . . . . . 14  |-  ( (
<. v ,  e >.  e. USGrph  /\  n  e.  v )  ->  ( v  \  { n } ) USGrph 
(  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } ) )
2716, 26sylanb 470 . . . . . . . . . . . . 13  |-  ( ( v USGrph  e  /\  n  e.  v )  ->  (
v  \  { n } ) USGrph  (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } ) )
28 eleq1 2468 . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . 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 32797 . . . . . . . . . . . . 13  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  0 )  ->  e  e.  Fin )
31 residfi 32674 . . . . . . . . . . . . . . . 16  |-  ( (  _I  |`  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p } )  e.  Fin  <->  {
p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  e.  Fin )
32 simpr1 1000 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
v USGrph  e )
33 eleq1 2468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  +  1 )  =  ( # `  v
)  ->  ( (
y  +  1 )  e.  NN0  <->  ( # `  v
)  e.  NN0 )
)
3433eqcoms 2408 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  v )  =  ( y  +  1 )  ->  (
( y  +  1 )  e.  NN0  <->  ( # `  v
)  e.  NN0 )
)
35 hashclb 12355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  e.  _V  ->  (
v  e.  Fin  <->  ( # `  v
)  e.  NN0 )
)
3635bicomd 201 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  e.  _V  ->  (
( # `  v )  e.  NN0  <->  v  e.  Fin ) )
3720, 36ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  v )  e.  NN0  <->  v  e.  Fin )
3837biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  v )  e.  NN0  ->  v  e.  Fin )
3934, 38syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  v )  =  ( y  +  1 )  ->  (
( y  +  1 )  e.  NN0  ->  v  e.  Fin ) )
40393ad2ant2 1016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  (
( y  +  1 )  e.  NN0  ->  v  e.  Fin ) )
4140impcom 428 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
v  e.  Fin )
4232, 41jca 530 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( v USGrph  e  /\  v  e.  Fin )
)
43 usgrav 24484 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v USGrph 
e  ->  ( v  e.  _V  /\  e  e. 
_V ) )
44 df-br 4385 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v FinUSGrph  e 
<-> 
<. v ,  e >.  e. FinUSGrph  )
45 isfusgra0 32782 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  _V  /\  e  e.  _V )  ->  ( v FinUSGrph  e  <->  ( v USGrph  e  /\  v  e.  Fin ) ) )
4644, 45syl5bbr 259 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  _V  /\  e  e.  _V )  ->  ( <. v ,  e
>.  e. FinUSGrph 
<->  ( v USGrph  e  /\  v  e.  Fin )
) )
4743, 46syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v USGrph 
e  ->  ( <. v ,  e >.  e. FinUSGrph  <->  ( v USGrph  e  /\  v  e.  Fin ) ) )
48473ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  ( <. v ,  e >.  e. FinUSGrph  <->  ( v USGrph  e  /\  v  e.  Fin ) ) )
4948adantl 464 . . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  ->  <. v ,  e >.  e. FinUSGrph  )
5117, 18mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v USGrph 
e  ->  ( Vtx  `  <. v ,  e >. )  =  ( 1st `  <. v ,  e >. )
)
5251, 22syl6req 2454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v USGrph 
e  ->  v  =  ( Vtx  `  <. v ,  e
>. ) )
5352eleq2d 2466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v USGrph 
e  ->  ( n  e.  v  <->  n  e.  ( Vtx  ` 
<. v ,  e >.
) ) )
5453biimpd 207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v USGrph 
e  ->  ( n  e.  v  ->  n  e.  ( Vtx  `  <. v ,  e >. ) ) )
5554a1d 25 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v USGrph 
e  ->  ( ( # `
 v )  =  ( y  +  1 )  ->  ( n  e.  v  ->  n  e.  ( Vtx  `  <. v ,  e >. ) ) ) )
56553imp 1188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  n  e.  ( Vtx  `  <. v ,  e >. )
)
5756adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  ->  n  e.  ( Vtx  `  <. v ,  e >. )
)
5850, 57jca 530 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( <. v ,  e
>.  e. FinUSGrph  /\  n  e.  ( Vtx  `  <. v ,  e
>. ) ) )
59 eqid 2396 . . . . . . . . . . . . . . . . . . 19  |-  ( Vtx  `  <. v ,  e >.
)  =  ( Vtx  `  <. v ,  e >.
)
60 df-ov 6221 . . . . . . . . . . . . . . . . . . 19  |-  ( v Edges 
e )  =  ( Edges  `  <. v ,  e
>. )
6160eqcomi 2409 . . . . . . . . . . . . . . . . . . . 20  |-  ( Edges  `  <. v ,  e >. )  =  ( v Edges  e
)
62 rabeq 3045 . . . . . . . . . . . . . . . . . . . 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 32802 . . . . . . . . . . . . . . . . . 18  |-  ( (
<. v ,  e >.  e. FinUSGrph 
/\  n  e.  ( Vtx  `  <. v ,  e
>. ) )  ->  (
( v Edges  e )  e.  Fin  <->  { p  e.  ( Edges  `  <. v ,  e >. )  |  n  e/  p }  e.  Fin )
)
6558, 64syl 16 . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . 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 427 . . . . . . . . . . . . . 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 32791 . . . . . . . . . . . . . . . . 17  |-  ( v USGrph 
e  ->  ( e  e.  Fin  <->  ( v Edges  e
)  e.  Fin )
)
70693ad2ant1 1015 . . . . . . . . . . . . . . . 16  |-  ( ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v )  ->  (
e  e.  Fin  <->  ( v Edges  e )  e.  Fin ) )
7170adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v USGrph  e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )  -> 
( e  e.  Fin  <->  (
v Edges  e )  e. 
Fin ) )
7271adantr 463 . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . 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 12460 . . . . . . . . . . . 12  |-  ( ( ( 1st `  G
) USGrph  ( 2nd `  G
)  /\  ( 1st `  G )  e.  Fin )  ->  ( 2nd `  G
)  e.  Fin )
7574ex 432 . . . . . . . . . . 11  |-  ( ( 1st `  G ) USGrph 
( 2nd `  G
)  ->  ( ( 1st `  G )  e. 
Fin  ->  ( 2nd `  G
)  e.  Fin )
)
767, 75syl6bi 228 . . . . . . . . . 10  |-  ( G  =  <. ( 1st `  G
) ,  ( 2nd `  G ) >.  ->  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( 2nd `  G )  e. 
Fin ) ) )
774, 76mpcom 36 . . . . . . . . 9  |-  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( 2nd `  G
)  e.  Fin )
)
7877imp 427 . . . . . . . 8  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  ( 2nd `  G )  e. 
Fin )
79 rnfi 7742 . . . . . . . 8  |-  ( ( 2nd `  G )  e.  Fin  ->  ran  ( 2nd `  G )  e.  Fin )
8078, 79syl 16 . . . . . . 7  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  ran  ( 2nd `  G )  e.  Fin )
81 edgval 24485 . . . . . . . . 9  |-  ( G  e. USGrph  ->  ( Edges  `  G )  =  ran  ( 2nd `  G ) )
8281eleq1d 2465 . . . . . . . 8  |-  ( G  e. USGrph  ->  ( ( Edges  `  G
)  e.  Fin  <->  ran  ( 2nd `  G )  e.  Fin ) )
8382adantr 463 . . . . . . 7  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  (
( Edges  `  G )  e. 
Fin 
<->  ran  ( 2nd `  G
)  e.  Fin )
)
8480, 83mpbird 232 . . . . . 6  |-  ( ( G  e. USGrph  /\  ( 1st `  G )  e. 
Fin )  ->  ( Edges  `  G )  e.  Fin )
8584ex 432 . . . . 5  |-  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( Edges  `  G )  e.  Fin ) )
8685a1dd 46 . . . 4  |-  ( G  e. USGrph  ->  ( ( 1st `  G )  e.  Fin  ->  ( G  e. FinUSGrph  ->  ( Edges  `  G )  e.  Fin ) ) )
87 gordval 32745 . . . . . 6  |-  ( G  e. USGrph  ->  ( GrOrder  `  G )  =  ( # `  ( 1st `  G ) ) )
8887eleq1d 2465 . . . . 5  |-  ( G  e. USGrph  ->  ( ( GrOrder  `  G
)  e.  NN0  <->  ( # `  ( 1st `  G ) )  e.  NN0 ) )
89 fvex 5801 . . . . . 6  |-  ( 1st `  G )  e.  _V
90 hashclb 12355 . . . . . 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 263 . . . 4  |-  ( G  e. USGrph  ->  ( ( GrOrder  `  G
)  e.  NN0  <->  ( 1st `  G )  e.  Fin ) )
93 usgsizedg 32752 . . . . . . 7  |-  ( G  e. USGrph  ->  ( GrSize  `  G )  =  ( # `  ( Edges  `  G ) ) )
9493eleq1d 2465 . . . . . 6  |-  ( G  e. USGrph  ->  ( ( GrSize  `  G
)  e.  NN0  <->  ( # `  ( Edges  `  G ) )  e. 
NN0 ) )
95 fvex 5801 . . . . . . 7  |-  ( Edges  `  G
)  e.  _V
96 hashclb 12355 . . . . . . 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 263 . . . . 5  |-  ( G  e. USGrph  ->  ( ( GrSize  `  G
)  e.  NN0  <->  ( Edges  `  G
)  e.  Fin )
)
9998imbi2d 314 . . . 4  |-  ( G  e. USGrph  ->  ( ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 )  <->  ( G  e. FinUSGrph 
->  ( Edges  `  G )  e.  Fin ) ) )
10086, 92, 993imtr4d 268 . . 3  |-  ( G  e. USGrph  ->  ( ( GrOrder  `  G
)  e.  NN0  ->  ( G  e. FinUSGrph  ->  ( GrSize  `  G
)  e.  NN0 )
) )
101100imp 427 . 2  |-  ( ( G  e. USGrph  /\  ( GrOrder  `  G )  e.  NN0 )  ->  ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 ) )
1021, 101mpcom 36 1  |-  ( G  e. FinUSGrph  ->  ( GrSize  `  G )  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1836    e/ wnel 2592   {crab 2750   _Vcvv 3051    \ cdif 3403   {csn 3961   <.cop 3967   class class class wbr 4384    |-> cmpt 4442    _I cid 4721   ran crn 4931    |` cres 4932   Rel wrel 4935   ` cfv 5513  (class class class)co 6218   1stc1st 6719   2ndc2nd 6720   Fincfn 7457   1c1 9426    + caddc 9428   NN0cn0 10734   #chash 12330   USGrph cusg 24476   Edges cedg 24477   Vtx cvtx 32738   GrOrder cgord 32741   GrSize cgsiz 32742   FinUSGrph cfusg 32778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-rep 4495  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-recs 6982  df-rdg 7016  df-1o 7070  df-2o 7071  df-oadd 7074  df-er 7251  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-card 8255  df-cda 8483  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-2 10533  df-n0 10735  df-z 10804  df-uz 11024  df-fz 11616  df-hash 12331  df-uhgra 24438  df-umgra 24459  df-uslgra 24478  df-usgra 24479  df-edg 24482  df-vtx 32739  df-gord 32743  df-gsiz 32744  df-fusg 32779
This theorem is referenced by:  usgrafiedgALT  32808
  Copyright terms: Public domain W3C validator