Metamath Proof Explorer

Theorem supnfcls

Description: The filter of supersets of X \ U does not cluster at any point of the open set U . (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion supnfcls 
|- ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) -> -. A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) )

Proof

Step Hyp Ref Expression
1 disjdif 
 |-  ( U i^i ( X \ U ) ) = (/)
2 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) )
3 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> U e. J )
4 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> A e. U )
5 sseq2 
 |-  ( x = ( X \ U ) -> ( ( X \ U ) C_ x <-> ( X \ U ) C_ ( X \ U ) ) )
6 difss 
 |-  ( X \ U ) C_ X
7 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> J e. ( TopOn ` X ) )
8 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
9 elpw2g 
 |-  ( X e. J -> ( ( X \ U ) e. ~P X <-> ( X \ U ) C_ X ) )
10 7 8 9 3syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> ( ( X \ U ) e. ~P X <-> ( X \ U ) C_ X ) )
11 6 10 mpbiri 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> ( X \ U ) e. ~P X )
12 ssidd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> ( X \ U ) C_ ( X \ U ) )
13 5 11 12 elrabd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> ( X \ U ) e. { x e. ~P X | ( X \ U ) C_ x } )
14 fclsopni 
 |-  ( ( A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) /\ ( U e. J /\ A e. U /\ ( X \ U ) e. { x e. ~P X | ( X \ U ) C_ x } ) ) -> ( U i^i ( X \ U ) ) =/= (/) )
15 2 3 4 13 14 syl13anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) /\ A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) -> ( U i^i ( X \ U ) ) =/= (/) )
16 15 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) -> ( A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) -> ( U i^i ( X \ U ) ) =/= (/) ) )
17 16 necon2bd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) -> ( ( U i^i ( X \ U ) ) = (/) -> -. A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) ) )
18 1 17 mpi 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. U ) -> -. A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) )