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 
|- X = U. R
txcmpb.2 
|- Y = U. S
Assertion txcmpb 
|- ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( R tX S ) e. Comp <-> ( R e. Comp /\ S e. Comp ) ) )

Proof

Step Hyp Ref Expression
1 txcmpb.1 
 |-  X = U. R
2 txcmpb.2 
 |-  Y = U. S
3 simpr 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( R tX S ) e. Comp )
4 simplrr 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> Y =/= (/) )
5 fo1stres 
 |-  ( Y =/= (/) -> ( 1st |` ( X X. Y ) ) : ( X X. Y ) -onto-> X )
6 4 5 syl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( 1st |` ( X X. Y ) ) : ( X X. Y ) -onto-> X )
7 1 2 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
8 7 ad2antrr 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( X X. Y ) = U. ( R tX S ) )
9 foeq2 
 |-  ( ( X X. Y ) = U. ( R tX S ) -> ( ( 1st |` ( X X. Y ) ) : ( X X. Y ) -onto-> X <-> ( 1st |` ( X X. Y ) ) : U. ( R tX S ) -onto-> X ) )
10 8 9 syl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( ( 1st |` ( X X. Y ) ) : ( X X. Y ) -onto-> X <-> ( 1st |` ( X X. Y ) ) : U. ( R tX S ) -onto-> X ) )
11 6 10 mpbid 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( 1st |` ( X X. Y ) ) : U. ( R tX S ) -onto-> X )
12 1 toptopon 
 |-  ( R e. Top <-> R e. ( TopOn ` X ) )
13 2 toptopon 
 |-  ( S e. Top <-> S e. ( TopOn ` Y ) )
14 tx1cn 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
15 12 13 14 syl2anb 
 |-  ( ( R e. Top /\ S e. Top ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
16 15 ad2antrr 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
17 1 cncmp 
 |-  ( ( ( R tX S ) e. Comp /\ ( 1st |` ( X X. Y ) ) : U. ( R tX S ) -onto-> X /\ ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) ) -> R e. Comp )
18 3 11 16 17 syl3anc 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> R e. Comp )
19 simplrl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> X =/= (/) )
20 fo2ndres 
 |-  ( X =/= (/) -> ( 2nd |` ( X X. Y ) ) : ( X X. Y ) -onto-> Y )
21 19 20 syl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( 2nd |` ( X X. Y ) ) : ( X X. Y ) -onto-> Y )
22 foeq2 
 |-  ( ( X X. Y ) = U. ( R tX S ) -> ( ( 2nd |` ( X X. Y ) ) : ( X X. Y ) -onto-> Y <-> ( 2nd |` ( X X. Y ) ) : U. ( R tX S ) -onto-> Y ) )
23 8 22 syl 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( ( 2nd |` ( X X. Y ) ) : ( X X. Y ) -onto-> Y <-> ( 2nd |` ( X X. Y ) ) : U. ( R tX S ) -onto-> Y ) )
24 21 23 mpbid 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( 2nd |` ( X X. Y ) ) : U. ( R tX S ) -onto-> Y )
25 tx2cn 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
26 12 13 25 syl2anb 
 |-  ( ( R e. Top /\ S e. Top ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
27 26 ad2antrr 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
28 2 cncmp 
 |-  ( ( ( R tX S ) e. Comp /\ ( 2nd |` ( X X. Y ) ) : U. ( R tX S ) -onto-> Y /\ ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) ) -> S e. Comp )
29 3 24 27 28 syl3anc 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> S e. Comp )
30 18 29 jca 
 |-  ( ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) /\ ( R tX S ) e. Comp ) -> ( R e. Comp /\ S e. Comp ) )
31 30 ex 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( R tX S ) e. Comp -> ( R e. Comp /\ S e. Comp ) ) )
32 txcmp 
 |-  ( ( R e. Comp /\ S e. Comp ) -> ( R tX S ) e. Comp )
33 31 32 impbid1 
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( R tX S ) e. Comp <-> ( R e. Comp /\ S e. Comp ) ) )