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=\mathrm{Vtx}\left(G\right)$$
	fusgrmaxsize.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
	usgrsscusgra.h	$$⊢V=\mathrm{Vtx}\left(H\right)$$
	usgrsscusgra.f	$$⊢F=\mathrm{Edg}\left(H\right)$$
Assertion	sizusglecusglem1	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{ComplUSGraph}\right)\to \left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1}{⟶}F$$

Proof

Step	Hyp	Ref	Expression
1		fusgrmaxsize.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		fusgrmaxsize.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		usgrsscusgra.h	$$⊢V=\mathrm{Vtx}\left(H\right)$$
4		usgrsscusgra.f	$$⊢F=\mathrm{Edg}\left(H\right)$$
5		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E$$
6		f1of1	$$⊢\left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E\to \left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1}{⟶}E$$
7	5 6	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1}{⟶}E$$
8	1 2 3 4	usgredgsscusgredg	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{ComplUSGraph}\right)\to E\subseteq F$$
9		f1ss	$$⊢\left(\left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1}{⟶}E\wedge E\subseteq F\right)\to \left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1}{⟶}F$$
10	7 8 9	sylancr	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{ComplUSGraph}\right)\to \left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1}{⟶}F$$