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

Metamath Proof Explorer

Theorem cmpcov

Description: An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009)

Ref Expression
Hypothesis iscmp.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cmpcov ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆 ) → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 )

Proof

Step Hyp Ref Expression
1 iscmp.1 ⊢ 𝑋 = ∪ 𝐽
2 unieq ⊢ ( 𝑟 = 𝑆 → ∪ 𝑟 = ∪ 𝑆 )
3 2 eqeq2d ⊢ ( 𝑟 = 𝑆 → ( 𝑋 = ∪ 𝑟 ↔ 𝑋 = ∪ 𝑆 ) )
4 pweq ⊢ ( 𝑟 = 𝑆 → 𝒫 𝑟 = 𝒫 𝑆 )
5 4 ineq1d ⊢ ( 𝑟 = 𝑆 → ( 𝒫 𝑟 ∩ Fin ) = ( 𝒫 𝑆 ∩ Fin ) )
6 5 rexeqdv ⊢ ( 𝑟 = 𝑆 → ( ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ↔ ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
7 3 6 imbi12d ⊢ ( 𝑟 = 𝑆 → ( ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ↔ ( 𝑋 = ∪ 𝑆 → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
8 1 iscmp ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
9 8 simprbi ⊢ ( 𝐽 ∈ Comp → ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
10 9 adantr ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
11 ssexg ⊢ ( ( 𝑆 ⊆ 𝐽 ∧ 𝐽 ∈ Comp ) → 𝑆 ∈ V )
12 11 ancoms ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → 𝑆 ∈ V )
13 simpr ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → 𝑆 ⊆ 𝐽 )
14 12 13 elpwd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → 𝑆 ∈ 𝒫 𝐽 )
15 7 10 14 rspcdva ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → ( 𝑋 = ∪ 𝑆 → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
16 15 3impia ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆 ) → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 )