Metamath Proof Explorer

Theorem cmpfiiin

Description: In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses cmpfiiin.x 
|- X = U. J
cmpfiiin.j 
|- ( ph -> J e. Comp )
cmpfiiin.s 
|- ( ( ph /\ k e. I ) -> S e. ( Clsd ` J ) )
cmpfiiin.z 
|- ( ( ph /\ ( l C_ I /\ l e. Fin ) ) -> ( X i^i |^|_ k e. l S ) =/= (/) )
Assertion cmpfiiin 
|- ( ph -> ( X i^i |^|_ k e. I S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 cmpfiiin.x 
 |-  X = U. J
2 cmpfiiin.j 
 |-  ( ph -> J e. Comp )
3 cmpfiiin.s 
 |-  ( ( ph /\ k e. I ) -> S e. ( Clsd ` J ) )
4 cmpfiiin.z 
 |-  ( ( ph /\ ( l C_ I /\ l e. Fin ) ) -> ( X i^i |^|_ k e. l S ) =/= (/) )
5 cmptop 
 |-  ( J e. Comp -> J e. Top )
6 2 5 syl 
 |-  ( ph -> J e. Top )
7 1 topcld 
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
8 6 7 syl 
 |-  ( ph -> X e. ( Clsd ` J ) )
9 1 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ X )
10 3 9 syl 
 |-  ( ( ph /\ k e. I ) -> S C_ X )
11 10 ralrimiva 
 |-  ( ph -> A. k e. I S C_ X )
12 riinint 
 |-  ( ( X e. ( Clsd ` J ) /\ A. k e. I S C_ X ) -> ( X i^i |^|_ k e. I S ) = |^| ( { X } u. ran ( k e. I |-> S ) ) )
13 8 11 12 syl2anc 
 |-  ( ph -> ( X i^i |^|_ k e. I S ) = |^| ( { X } u. ran ( k e. I |-> S ) ) )
14 8 snssd 
 |-  ( ph -> { X } C_ ( Clsd ` J ) )
15 3 fmpttd 
 |-  ( ph -> ( k e. I |-> S ) : I --> ( Clsd ` J ) )
16 15 frnd 
 |-  ( ph -> ran ( k e. I |-> S ) C_ ( Clsd ` J ) )
17 14 16 unssd 
 |-  ( ph -> ( { X } u. ran ( k e. I |-> S ) ) C_ ( Clsd ` J ) )
18 elin 
 |-  ( l e. ( ~P I i^i Fin ) <-> ( l e. ~P I /\ l e. Fin ) )
19 elpwi 
 |-  ( l e. ~P I -> l C_ I )
20 19 anim1i 
 |-  ( ( l e. ~P I /\ l e. Fin ) -> ( l C_ I /\ l e. Fin ) )
21 18 20 sylbi 
 |-  ( l e. ( ~P I i^i Fin ) -> ( l C_ I /\ l e. Fin ) )
22 nesym 
 |-  ( ( X i^i |^|_ k e. l S ) =/= (/) <-> -. (/) = ( X i^i |^|_ k e. l S ) )
23 4 22 sylib 
 |-  ( ( ph /\ ( l C_ I /\ l e. Fin ) ) -> -. (/) = ( X i^i |^|_ k e. l S ) )
24 21 23 sylan2 
 |-  ( ( ph /\ l e. ( ~P I i^i Fin ) ) -> -. (/) = ( X i^i |^|_ k e. l S ) )
25 24 nrexdv 
 |-  ( ph -> -. E. l e. ( ~P I i^i Fin ) (/) = ( X i^i |^|_ k e. l S ) )
26 elrfirn2 
 |-  ( ( X e. ( Clsd ` J ) /\ A. k e. I S C_ X ) -> ( (/) e. ( fi ` ( { X } u. ran ( k e. I |-> S ) ) ) <-> E. l e. ( ~P I i^i Fin ) (/) = ( X i^i |^|_ k e. l S ) ) )
27 8 11 26 syl2anc 
 |-  ( ph -> ( (/) e. ( fi ` ( { X } u. ran ( k e. I |-> S ) ) ) <-> E. l e. ( ~P I i^i Fin ) (/) = ( X i^i |^|_ k e. l S ) ) )
28 25 27 mtbird 
 |-  ( ph -> -. (/) e. ( fi ` ( { X } u. ran ( k e. I |-> S ) ) ) )
29 cmpfii 
 |-  ( ( J e. Comp /\ ( { X } u. ran ( k e. I |-> S ) ) C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` ( { X } u. ran ( k e. I |-> S ) ) ) ) -> |^| ( { X } u. ran ( k e. I |-> S ) ) =/= (/) )
30 2 17 28 29 syl3anc 
 |-  ( ph -> |^| ( { X } u. ran ( k e. I |-> S ) ) =/= (/) )
31 13 30 eqnetrd 
 |-  ( ph -> ( X i^i |^|_ k e. I S ) =/= (/) )