Step |
Hyp |
Ref |
Expression |
1 |
|
cusgrsizeindb0.v |
|- V = ( Vtx ` G ) |
2 |
|
cusgrsizeindb0.e |
|- E = ( Edg ` G ) |
3 |
1 2
|
usgr1v0e |
|- ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( # ` E ) = 0 ) |
4 |
|
oveq1 |
|- ( ( # ` V ) = 1 -> ( ( # ` V ) _C 2 ) = ( 1 _C 2 ) ) |
5 |
|
1nn0 |
|- 1 e. NN0 |
6 |
|
2z |
|- 2 e. ZZ |
7 |
|
1lt2 |
|- 1 < 2 |
8 |
7
|
olci |
|- ( 2 < 0 \/ 1 < 2 ) |
9 |
|
bcval4 |
|- ( ( 1 e. NN0 /\ 2 e. ZZ /\ ( 2 < 0 \/ 1 < 2 ) ) -> ( 1 _C 2 ) = 0 ) |
10 |
5 6 8 9
|
mp3an |
|- ( 1 _C 2 ) = 0 |
11 |
4 10
|
eqtrdi |
|- ( ( # ` V ) = 1 -> ( ( # ` V ) _C 2 ) = 0 ) |
12 |
11
|
eqeq2d |
|- ( ( # ` V ) = 1 -> ( ( # ` E ) = ( ( # ` V ) _C 2 ) <-> ( # ` E ) = 0 ) ) |
13 |
12
|
adantl |
|- ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( ( # ` E ) = ( ( # ` V ) _C 2 ) <-> ( # ` E ) = 0 ) ) |
14 |
3 13
|
mpbird |
|- ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) ) |