sizusglecusglem1

	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 \in USGraph \land H \in ComplUSGraph) \to ({I ↾}_{E}) : E \underset{1-1}{⟶} F$

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 \underset{1-1 onto}{⟶} E$
6		f1of1	$⊢ ({I ↾}_{E}) : E \underset{1-1 onto}{⟶} E \to ({I ↾}_{E}) : E \underset{1-1}{⟶} E$
7	5 6	ax-mp	$⊢ ({I ↾}_{E}) : E \underset{1-1}{⟶} E$
8	1 2 3 4	usgredgsscusgredg	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to E \subseteq F$
9		f1ss	$⊢ (({I ↾}_{E}) : E \underset{1-1}{⟶} E \land E \subseteq F) \to ({I ↾}_{E}) : E \underset{1-1}{⟶} F$
10	7 8 9	sylancr	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to ({I ↾}_{E}) : E \underset{1-1}{⟶} F$

Metamath Proof Explorer