Metamath Proof Explorer


Theorem sizusglecusglem1

Description: Lemma 1 for sizusglecusg . (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 13-Nov-2020)

Ref Expression
Hypotheses fusgrmaxsize.v
|- V = ( Vtx ` G )
fusgrmaxsize.e
|- E = ( Edg ` G )
usgrsscusgra.h
|- V = ( Vtx ` H )
usgrsscusgra.f
|- F = ( Edg ` H )
Assertion sizusglecusglem1
|- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( _I |` E ) : E -1-1-> F )

Proof

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 )