Metamath Proof Explorer

Theorem txcmpb

Description: The topological product of two nonempty topologies is compact iff the component topologies are both compact. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses txcmpb.1 ⊢ 𝑋 = ∪ 𝑅
txcmpb.2 ⊢ 𝑌 = ∪ 𝑆
Assertion txcmpb ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑅 ×t 𝑆 ) ∈ Comp ↔ ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ) )

Proof

Step Hyp Ref Expression
1 txcmpb.1 ⊢ 𝑋 = ∪ 𝑅
2 txcmpb.2 ⊢ 𝑌 = ∪ 𝑆
3 simpr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Comp )
4 simplrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑌 ≠ ∅ )
5 fo1stres ⊢ ( 𝑌 ≠ ∅ → ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 )
6 4 5 syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 )
7 1 2 txuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
8 7 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
9 foeq2 ⊢ ( ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 ↔ ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ) )
10 8 9 syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑋 ↔ ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ) )
11 6 10 mpbid ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 )
12 1 toptopon ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
13 2 toptopon ⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
14 tx1cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
15 12 13 14 syl2anb ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
16 15 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
17 1 cncmp ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Comp ∧ ( 1st ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑋 ∧ ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) → 𝑅 ∈ Comp )
18 3 11 16 17 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑅 ∈ Comp )
19 simplrl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑋 ≠ ∅ )
20 fo2ndres ⊢ ( 𝑋 ≠ ∅ → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 )
21 19 20 syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 )
22 foeq2 ⊢ ( ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ↔ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ) )
23 8 22 syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ↔ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ) )
24 21 23 mpbid ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 )
25 tx2cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
26 12 13 25 syl2anb ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
27 26 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
28 2 cncmp ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Comp ∧ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) : ∪ ( 𝑅 ×t 𝑆 ) –onto→ 𝑌 ∧ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) → 𝑆 ∈ Comp )
29 3 24 27 28 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → 𝑆 ∈ Comp )
30 18 29 jca ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ Comp ) → ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) )
31 30 ex ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑅 ×t 𝑆 ) ∈ Comp → ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ) )
32 txcmp ⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Comp )
33 31 32 impbid1 ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( ( 𝑅 ×t 𝑆 ) ∈ Comp ↔ ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ) )