Theorem sizusglecusglem2

Description: Lemma 2 for sizusglecusg . (Contributed by Alexander van der Vekens, 13-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	sizusglecusglem2	|- ( ( G e. USGraph /\ H e. ComplUSGraph /\ F e. Fin ) -> E e. Fin )

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