Metamath Proof Explorer


Theorem cmpfii

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
Assertion cmpfii
|- ( ( J e. Comp /\ X C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` X ) ) -> |^| X =/= (/) )

Proof

Step Hyp Ref Expression
1 fvex
 |-  ( Clsd ` J ) e. _V
2 1 elpw2
 |-  ( X e. ~P ( Clsd ` J ) <-> X C_ ( Clsd ` J ) )
3 2 biimpri
 |-  ( X C_ ( Clsd ` J ) -> X e. ~P ( Clsd ` J ) )
4 cmptop
 |-  ( J e. Comp -> J e. Top )
5 cmpfi
 |-  ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
6 4 5 syl
 |-  ( J e. Comp -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
7 6 ibi
 |-  ( J e. Comp -> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) )
8 fveq2
 |-  ( x = X -> ( fi ` x ) = ( fi ` X ) )
9 8 eleq2d
 |-  ( x = X -> ( (/) e. ( fi ` x ) <-> (/) e. ( fi ` X ) ) )
10 9 notbid
 |-  ( x = X -> ( -. (/) e. ( fi ` x ) <-> -. (/) e. ( fi ` X ) ) )
11 inteq
 |-  ( x = X -> |^| x = |^| X )
12 11 neeq1d
 |-  ( x = X -> ( |^| x =/= (/) <-> |^| X =/= (/) ) )
13 10 12 imbi12d
 |-  ( x = X -> ( ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) <-> ( -. (/) e. ( fi ` X ) -> |^| X =/= (/) ) ) )
14 13 rspcva
 |-  ( ( X e. ~P ( Clsd ` J ) /\ A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) -> ( -. (/) e. ( fi ` X ) -> |^| X =/= (/) ) )
15 3 7 14 syl2anr
 |-  ( ( J e. Comp /\ X C_ ( Clsd ` J ) ) -> ( -. (/) e. ( fi ` X ) -> |^| X =/= (/) ) )
16 15 3impia
 |-  ( ( J e. Comp /\ X C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` X ) ) -> |^| X =/= (/) )