Metamath Proof Explorer

Theorem txcmp

Description: The topological product of two compact spaces is compact. (Contributed by Mario Carneiro, 14-Sep-2014) (Proof shortened 21-Mar-2015.)

Ref Expression
Assertion txcmp ⊢ R ∈ Comp ∧ S ∈ Comp → R × t S ∈ Comp

Proof

Step Hyp Ref Expression
1 cmptop ⊢ R ∈ Comp → R ∈ Top
2 cmptop ⊢ S ∈ Comp → S ∈ Top
3 txtop ⊢ R ∈ Top ∧ S ∈ Top → R × t S ∈ Top
4 1 2 3 syl2an ⊢ R ∈ Comp ∧ S ∈ Comp → R × t S ∈ Top
5 eqid ⊢ ⋃ R = ⋃ R
6 eqid ⊢ ⋃ S = ⋃ S
7 simpll ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → R ∈ Comp
8 simplr ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → S ∈ Comp
9 elpwi ⊢ w ∈ 𝒫 R × t S → w ⊆ R × t S
10 9 ad2antrl ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → w ⊆ R × t S
11 5 6 txuni ⊢ R ∈ Top ∧ S ∈ Top → ⋃ R × ⋃ S = ⋃ R × t S
12 1 2 11 syl2an ⊢ R ∈ Comp ∧ S ∈ Comp → ⋃ R × ⋃ S = ⋃ R × t S
13 12 adantr ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ⋃ R × ⋃ S = ⋃ R × t S
14 simprr ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ⋃ R × t S = ⋃ w
15 13 14 eqtrd ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ⋃ R × ⋃ S = ⋃ w
16 5 6 7 8 10 15 txcmplem2 ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × ⋃ S = ⋃ v
17 13 eqeq1d ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ⋃ R × ⋃ S = ⋃ v ↔ ⋃ R × t S = ⋃ v
18 17 rexbidv ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × ⋃ S = ⋃ v ↔ ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × t S = ⋃ v
19 16 18 mpbid ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S ∧ ⋃ R × t S = ⋃ w → ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × t S = ⋃ v
20 19 expr ⊢ R ∈ Comp ∧ S ∈ Comp ∧ w ∈ 𝒫 R × t S → ⋃ R × t S = ⋃ w → ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × t S = ⋃ v
21 20 ralrimiva ⊢ R ∈ Comp ∧ S ∈ Comp → ∀ w ∈ 𝒫 R × t S ⋃ R × t S = ⋃ w → ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × t S = ⋃ v
22 eqid ⊢ ⋃ R × t S = ⋃ R × t S
23 22 iscmp ⊢ R × t S ∈ Comp ↔ R × t S ∈ Top ∧ ∀ w ∈ 𝒫 R × t S ⋃ R × t S = ⋃ w → ∃ v ∈ 𝒫 w ∩ Fin ⋃ R × t S = ⋃ v
24 4 21 23 sylanbrc ⊢ R ∈ Comp ∧ S ∈ Comp → R × t S ∈ Comp