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

Metamath Proof Explorer

Theorem iscmp

Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis iscmp.1 ⊢ X = ⋃ J
Assertion iscmp ⊢ J ∈ Comp ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin X = ⋃ z

Proof

Step Hyp Ref Expression
1 iscmp.1 ⊢ X = ⋃ J
2 pweq ⊢ x = J → 𝒫 x = 𝒫 J
3 unieq ⊢ x = J → ⋃ x = ⋃ J
4 3 1 eqtr4di ⊢ x = J → ⋃ x = X
5 4 eqeq1d ⊢ x = J → ⋃ x = ⋃ y ↔ X = ⋃ y
6 4 eqeq1d ⊢ x = J → ⋃ x = ⋃ z ↔ X = ⋃ z
7 6 rexbidv ⊢ x = J → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z ↔ ∃ z ∈ 𝒫 y ∩ Fin X = ⋃ z
8 5 7 imbi12d ⊢ x = J → ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z ↔ X = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin X = ⋃ z
9 2 8 raleqbidv ⊢ x = J → ∀ y ∈ 𝒫 x ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z ↔ ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin X = ⋃ z
10 df-cmp ⊢ Comp = x ∈ Top | ∀ y ∈ 𝒫 x ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
11 9 10 elrab2 ⊢ J ∈ Comp ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin X = ⋃ z