sizusglecusglem2

	Ref	Expression
Hypotheses	fusgrmaxsize.v	$⊢ V = Vtx (G)$
	fusgrmaxsize.e	$⊢ E = Edg (G)$
	usgrsscusgra.h	$⊢ V = Vtx (H)$
	usgrsscusgra.f	$⊢ F = Edg (H)$
Assertion	sizusglecusglem2	$⊢ (G \in USGraph \land H \in ComplUSGraph \land F \in Fin) \to E \in Fin$

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	3 4	cusgrfi	$⊢ (H \in ComplUSGraph \land F \in Fin) \to V \in Fin$
6	5	3adant1	$⊢ (G \in USGraph \land H \in ComplUSGraph \land F \in Fin) \to V \in Fin$
7	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land V \in Fin)$
8		fusgrfis	$⊢ G \in FinUSGraph \to Edg (G) \in Fin$
9	7 8	sylbir	$⊢ (G \in USGraph \land V \in Fin) \to Edg (G) \in Fin$
10	2 9	eqeltrid	$⊢ (G \in USGraph \land V \in Fin) \to E \in Fin$
11	10	ex	$⊢ G \in USGraph \to (V \in Fin \to E \in Fin)$
12	11	3ad2ant1	$⊢ (G \in USGraph \land H \in ComplUSGraph \land F \in Fin) \to (V \in Fin \to E \in Fin)$
13	6 12	mpd	$⊢ (G \in USGraph \land H \in ComplUSGraph \land F \in Fin) \to E \in Fin$

Metamath Proof Explorer