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 ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Comp )

Proof

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