This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )