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 ) ) )