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 ⊢ 𝑋 = ∪ 𝐽
Assertion iscmp ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 iscmp.1 ⊢ 𝑋 = ∪ 𝐽
2 pweq ⊢ ( 𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽 )
3 unieq ⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽 )
4 3 1 eqtr4di ⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = 𝑋 )
5 4 eqeq1d ⊢ ( 𝑥 = 𝐽 → ( ∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦 ) )
6 4 eqeq1d ⊢ ( 𝑥 = 𝐽 → ( ∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧 ) )
7 6 rexbidv ⊢ ( 𝑥 = 𝐽 → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
8 5 7 imbi12d ⊢ ( 𝑥 = 𝐽 → ( ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) ↔ ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
9 2 8 raleqbidv ⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
10 df-cmp ⊢ Comp = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
11 9 10 elrab2 ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )