This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmpcov

Description: An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009)

Ref Expression
Hypothesis iscmp.1 
|- X = U. J
Assertion cmpcov 
|- ( ( J e. Comp /\ S C_ J /\ X = U. S ) -> E. s e. ( ~P S i^i Fin ) X = U. s )

Proof

Step Hyp Ref Expression
1 iscmp.1 
 |-  X = U. J
2 unieq 
 |-  ( r = S -> U. r = U. S )
3 2 eqeq2d 
 |-  ( r = S -> ( X = U. r <-> X = U. S ) )
4 pweq 
 |-  ( r = S -> ~P r = ~P S )
5 4 ineq1d 
 |-  ( r = S -> ( ~P r i^i Fin ) = ( ~P S i^i Fin ) )
6 5 rexeqdv 
 |-  ( r = S -> ( E. s e. ( ~P r i^i Fin ) X = U. s <-> E. s e. ( ~P S i^i Fin ) X = U. s ) )
7 3 6 imbi12d 
 |-  ( r = S -> ( ( X = U. r -> E. s e. ( ~P r i^i Fin ) X = U. s ) <-> ( X = U. S -> E. s e. ( ~P S i^i Fin ) X = U. s ) ) )
8 1 iscmp 
 |-  ( J e. Comp <-> ( J e. Top /\ A. r e. ~P J ( X = U. r -> E. s e. ( ~P r i^i Fin ) X = U. s ) ) )
9 8 simprbi 
 |-  ( J e. Comp -> A. r e. ~P J ( X = U. r -> E. s e. ( ~P r i^i Fin ) X = U. s ) )
10 9 adantr 
 |-  ( ( J e. Comp /\ S C_ J ) -> A. r e. ~P J ( X = U. r -> E. s e. ( ~P r i^i Fin ) X = U. s ) )
11 ssexg 
 |-  ( ( S C_ J /\ J e. Comp ) -> S e. _V )
12 11 ancoms 
 |-  ( ( J e. Comp /\ S C_ J ) -> S e. _V )
13 simpr 
 |-  ( ( J e. Comp /\ S C_ J ) -> S C_ J )
14 12 13 elpwd 
 |-  ( ( J e. Comp /\ S C_ J ) -> S e. ~P J )
15 7 10 14 rspcdva 
 |-  ( ( J e. Comp /\ S C_ J ) -> ( X = U. S -> E. s e. ( ~P S i^i Fin ) X = U. s ) )
16 15 3impia 
 |-  ( ( J e. Comp /\ S C_ J /\ X = U. S ) -> E. s e. ( ~P S i^i Fin ) X = U. s )