Metamath Proof Explorer

Theorem fincmp

Description: A finite topology is compact. (Contributed by FL, 22-Dec-2008)

Ref Expression
Assertion fincmp ⊢ J ∈ Top ∩ Fin → J ∈ Comp

Proof

Step Hyp Ref Expression
1 elinel1 ⊢ J ∈ Top ∩ Fin → J ∈ Top
2 elinel2 ⊢ J ∈ Top ∩ Fin → J ∈ Fin
3 vex ⊢ y ∈ V
4 3 pwid ⊢ y ∈ 𝒫 y
5 velpw ⊢ y ∈ 𝒫 J ↔ y ⊆ J
6 ssfi ⊢ J ∈ Fin ∧ y ⊆ J → y ∈ Fin
7 5 6 sylan2b ⊢ J ∈ Fin ∧ y ∈ 𝒫 J → y ∈ Fin
8 elin ⊢ y ∈ 𝒫 y ∩ Fin ↔ y ∈ 𝒫 y ∧ y ∈ Fin
9 unieq ⊢ z = y → ⋃ z = ⋃ y
10 9 rspceeqv ⊢ y ∈ 𝒫 y ∩ Fin ∧ ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
11 10 ex ⊢ y ∈ 𝒫 y ∩ Fin → ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
12 8 11 sylbir ⊢ y ∈ 𝒫 y ∧ y ∈ Fin → ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
13 4 7 12 sylancr ⊢ J ∈ Fin ∧ y ∈ 𝒫 J → ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
14 13 ralrimiva ⊢ J ∈ Fin → ∀ y ∈ 𝒫 J ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
15 2 14 syl ⊢ J ∈ Top ∩ Fin → ∀ y ∈ 𝒫 J ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
16 eqid ⊢ ⋃ J = ⋃ J
17 16 iscmp ⊢ J ∈ Comp ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 J ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
18 1 15 17 sylanbrc ⊢ J ∈ Top ∩ Fin → J ∈ Comp