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 )