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 
|- ( ( R e. Comp /\ S e. Comp ) -> ( R tX S ) e. Comp )

Proof

Step Hyp Ref Expression
1 cmptop 
 |-  ( R e. Comp -> R e. Top )
2 cmptop 
 |-  ( S e. Comp -> S e. Top )
3 txtop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4 1 2 3 syl2an 
 |-  ( ( R e. Comp /\ S e. Comp ) -> ( R tX S ) e. Top )
5 eqid 
 |-  U. R = U. R
6 eqid 
 |-  U. S = U. S
7 simpll 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> R e. Comp )
8 simplr 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> S e. Comp )
9 elpwi 
 |-  ( w e. ~P ( R tX S ) -> w C_ ( R tX S ) )
10 9 ad2antrl 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> w C_ ( R tX S ) )
11 5 6 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
12 1 2 11 syl2an 
 |-  ( ( R e. Comp /\ S e. Comp ) -> ( U. R X. U. S ) = U. ( R tX S ) )
13 12 adantr 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> ( U. R X. U. S ) = U. ( R tX S ) )
14 simprr 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> U. ( R tX S ) = U. w )
15 13 14 eqtrd 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> ( U. R X. U. S ) = U. w )
16 5 6 7 8 10 15 txcmplem2 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> E. v e. ( ~P w i^i Fin ) ( U. R X. U. S ) = U. v )
17 13 eqeq1d 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> ( ( U. R X. U. S ) = U. v <-> U. ( R tX S ) = U. v ) )
18 17 rexbidv 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> ( E. v e. ( ~P w i^i Fin ) ( U. R X. U. S ) = U. v <-> E. v e. ( ~P w i^i Fin ) U. ( R tX S ) = U. v ) )
19 16 18 mpbid 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ ( w e. ~P ( R tX S ) /\ U. ( R tX S ) = U. w ) ) -> E. v e. ( ~P w i^i Fin ) U. ( R tX S ) = U. v )
20 19 expr 
 |-  ( ( ( R e. Comp /\ S e. Comp ) /\ w e. ~P ( R tX S ) ) -> ( U. ( R tX S ) = U. w -> E. v e. ( ~P w i^i Fin ) U. ( R tX S ) = U. v ) )
21 20 ralrimiva 
 |-  ( ( R e. Comp /\ S e. Comp ) -> A. w e. ~P ( R tX S ) ( U. ( R tX S ) = U. w -> E. v e. ( ~P w i^i Fin ) U. ( R tX S ) = U. v ) )
22 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
23 22 iscmp 
 |-  ( ( R tX S ) e. Comp <-> ( ( R tX S ) e. Top /\ A. w e. ~P ( R tX S ) ( U. ( R tX S ) = U. w -> E. v e. ( ~P w i^i Fin ) U. ( R tX S ) = U. v ) ) )
24 4 21 23 sylanbrc 
 |-  ( ( R e. Comp /\ S e. Comp ) -> ( R tX S ) e. Comp )