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 )