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 \in TopOn (X) \land U \in J \land A \in U) \to \neg A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})$

Proof

Step	Hyp	Ref	Expression
1		disjdif	$⊢ U \cap (X ∖ U) = \emptyset$
2		simpr	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})$
3		simpl2	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to U \in J$
4		simpl3	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to A \in U$
5		sseq2	$⊢ x = X ∖ U \to (X ∖ U \subseteq x \leftrightarrow X ∖ U \subseteq X ∖ U)$
6		difss	$⊢ X ∖ U \subseteq X$
7		simpl1	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to J \in TopOn (X)$
8		toponmax	$⊢ J \in TopOn (X) \to X \in J$
9		elpw2g	$⊢ X \in J \to (X ∖ U \in 𝒫 X \leftrightarrow X ∖ U \subseteq X)$
10	7 8 9	3syl	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to (X ∖ U \in 𝒫 X \leftrightarrow X ∖ U \subseteq X)$
11	6 10	mpbiri	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to X ∖ U \in 𝒫 X$
12		ssidd	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to X ∖ U \subseteq X ∖ U$
13	5 11 12	elrabd	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to X ∖ U \in \{x \in 𝒫 X \| X ∖ U \subseteq x\}$
14		fclsopni	$⊢ (A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\}) \land (U \in J \land A \in U \land X ∖ U \in \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to U \cap (X ∖ U) \neq \emptyset$
15	2 3 4 13 14	syl13anc	$⊢ ((J \in TopOn (X) \land U \in J \land A \in U) \land A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})) \to U \cap (X ∖ U) \neq \emptyset$
16	15	ex	$⊢ (J \in TopOn (X) \land U \in J \land A \in U) \to (A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\}) \to U \cap (X ∖ U) \neq \emptyset)$
17	16	necon2bd	$⊢ (J \in TopOn (X) \land U \in J \land A \in U) \to (U \cap (X ∖ U) = \emptyset \to \neg A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\}))$
18	1 17	mpi	$⊢ (J \in TopOn (X) \land U \in J \land A \in U) \to \neg A \in (J fClus \{x \in 𝒫 X \| X ∖ U \subseteq x\})$