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

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 ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U → ¬ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x

Proof

Step Hyp Ref Expression
1 disjdif ⊢ U ∩ X ∖ U = ∅
2 simpr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x
3 simpl2 ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → U ∈ J
4 simpl3 ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → A ∈ U
5 sseq2 ⊢ x = X ∖ U → X ∖ U ⊆ x ↔ X ∖ U ⊆ X ∖ U
6 difss ⊢ X ∖ U ⊆ X
7 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → J ∈ TopOn ⁡ X
8 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
9 elpw2g ⊢ X ∈ J → X ∖ U ∈ 𝒫 X ↔ X ∖ U ⊆ X
10 7 8 9 3syl ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → X ∖ U ∈ 𝒫 X ↔ X ∖ U ⊆ X
11 6 10 mpbiri ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → X ∖ U ∈ 𝒫 X
12 ssidd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → X ∖ U ⊆ X ∖ U
13 5 11 12 elrabd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → X ∖ U ∈ x ∈ 𝒫 X | X ∖ U ⊆ x
14 fclsopni ⊢ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x ∧ U ∈ J ∧ A ∈ U ∧ X ∖ U ∈ x ∈ 𝒫 X | X ∖ U ⊆ x → U ∩ X ∖ U ≠ ∅
15 2 3 4 13 14 syl13anc ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U ∧ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → U ∩ X ∖ U ≠ ∅
16 15 ex ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U → A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x → U ∩ X ∖ U ≠ ∅
17 16 necon2bd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U → U ∩ X ∖ U = ∅ → ¬ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x
18 1 17 mpi ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ A ∈ U → ¬ A ∈ J fClus x ∈ 𝒫 X | X ∖ U ⊆ x