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

Metamath Proof Explorer

Theorem fincmp

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

Ref Expression
Assertion fincmp ( 𝐽 ∈ ( Top ∩ Fin ) → 𝐽 ∈ Comp )

Proof

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