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 ⊢ V = Vtx ⁡ G
fusgrmaxsize.e ⊢ E = Edg ⁡ G
usgrsscusgra.h ⊢ V = Vtx ⁡ H
usgrsscusgra.f ⊢ F = Edg ⁡ H
Assertion sizusglecusglem2 ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph ∧ F ∈ Fin → 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 ∈ ComplUSGraph ∧ F ∈ Fin → V ∈ Fin
6 5 3adant1 ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph ∧ F ∈ Fin → V ∈ Fin
7 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin
8 fusgrfis ⊢ G ∈ FinUSGraph → Edg ⁡ G ∈ Fin
9 7 8 sylbir ⊢ G ∈ USGraph ∧ V ∈ Fin → Edg ⁡ G ∈ Fin
10 2 9 eqeltrid ⊢ G ∈ USGraph ∧ V ∈ Fin → E ∈ Fin
11 10 ex ⊢ G ∈ USGraph → V ∈ Fin → E ∈ Fin
12 11 3ad2ant1 ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph ∧ F ∈ Fin → V ∈ Fin → E ∈ Fin
13 6 12 mpd ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph ∧ F ∈ Fin → E ∈ Fin