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

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 =/= (/) )