This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )