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