Step |
Hyp |
Ref |
Expression |
1 |
|
fusgrmaxsize.v |
|- V = ( Vtx ` G ) |
2 |
|
fusgrmaxsize.e |
|- E = ( Edg ` G ) |
3 |
|
usgrsscusgra.h |
|- V = ( Vtx ` H ) |
4 |
|
usgrsscusgra.f |
|- F = ( Edg ` H ) |
5 |
|
f1oi |
|- ( _I |` E ) : E -1-1-onto-> E |
6 |
|
f1of1 |
|- ( ( _I |` E ) : E -1-1-onto-> E -> ( _I |` E ) : E -1-1-> E ) |
7 |
5 6
|
ax-mp |
|- ( _I |` E ) : E -1-1-> E |
8 |
1 2 3 4
|
usgredgsscusgredg |
|- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> E C_ F ) |
9 |
|
f1ss |
|- ( ( ( _I |` E ) : E -1-1-> E /\ E C_ F ) -> ( _I |` E ) : E -1-1-> F ) |
10 |
7 8 9
|
sylancr |
|- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( _I |` E ) : E -1-1-> F ) |