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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgrmaxsize.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	usgrsscusgra.h	⊢ 𝑉 = ( Vtx ‘ 𝐻 )
	usgrsscusgra.f	⊢ 𝐹 = ( Edg ‘ 𝐻 )
Assertion	sizusglecusglem2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → 𝐸 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fusgrmaxsize.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgrmaxsize.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		usgrsscusgra.h	⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4		usgrsscusgra.f	⊢ 𝐹 = ( Edg ‘ 𝐻 )
5	3 4	cusgrfi	⊢ ( ( 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → 𝑉 ∈ Fin )
6	5	3adant1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → 𝑉 ∈ Fin )
7	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
8		fusgrfis	⊢ ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin )
9	7 8	sylbir	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ( Edg ‘ 𝐺 ) ∈ Fin )
10	2 9	eqeltrid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → 𝐸 ∈ Fin )
11	10	ex	⊢ ( 𝐺 ∈ USGraph → ( 𝑉 ∈ Fin → 𝐸 ∈ Fin ) )
12	11	3ad2ant1	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → ( 𝑉 ∈ Fin → 𝐸 ∈ Fin ) )
13	6 12	mpd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → 𝐸 ∈ Fin )