trnei

Description: The trace, over a set A , of the filter of the neighborhoods of a point P is a filter iff P belongs to the closure of A . (This is trfil2 applied to a filter of neighborhoods.) (Contributed by FL, 15-Sep-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	trnei	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to (P \in cls (J) (A) \leftrightarrow nei (J) (\{P\}) ↾_{𝑡} A \in Fil (A))$

Proof

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (Y) \to J \in Top$
2	1	3ad2ant1	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to J \in Top$
3		simp2	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to A \subseteq Y$
4		toponuni	$⊢ J \in TopOn (Y) \to Y = ⋃ J$
5	4	3ad2ant1	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to Y = ⋃ J$
6	3 5	sseqtrd	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to A \subseteq ⋃ J$
7		simp3	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to P \in Y$
8	7 5	eleqtrd	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to P \in ⋃ J$
9		eqid	$⊢ ⋃ J = ⋃ J$
10	9	neindisj2	$⊢ (J \in Top \land A \subseteq ⋃ J \land P \in ⋃ J) \to (P \in cls (J) (A) \leftrightarrow \forall v \in nei (J) (\{P\}) v \cap A \neq \emptyset)$
11	2 6 8 10	syl3anc	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to (P \in cls (J) (A) \leftrightarrow \forall v \in nei (J) (\{P\}) v \cap A \neq \emptyset)$
12		simp1	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to J \in TopOn (Y)$
13	7	snssd	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to \{P\} \subseteq Y$
14		snnzg	$⊢ P \in Y \to \{P\} \neq \emptyset$
15	14	3ad2ant3	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to \{P\} \neq \emptyset$
16		neifil	$⊢ (J \in TopOn (Y) \land \{P\} \subseteq Y \land \{P\} \neq \emptyset) \to nei (J) (\{P\}) \in Fil (Y)$
17	12 13 15 16	syl3anc	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to nei (J) (\{P\}) \in Fil (Y)$
18		trfil2	$⊢ (nei (J) (\{P\}) \in Fil (Y) \land A \subseteq Y) \to (nei (J) (\{P\}) ↾_{𝑡} A \in Fil (A) \leftrightarrow \forall v \in nei (J) (\{P\}) v \cap A \neq \emptyset)$
19	17 3 18	syl2anc	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to (nei (J) (\{P\}) ↾_{𝑡} A \in Fil (A) \leftrightarrow \forall v \in nei (J) (\{P\}) v \cap A \neq \emptyset)$
20	11 19	bitr4d	$⊢ (J \in TopOn (Y) \land A \subseteq Y \land P \in Y) \to (P \in cls (J) (A) \leftrightarrow nei (J) (\{P\}) ↾_{𝑡} A \in Fil (A))$

Metamath Proof Explorer

Theorem trnei

Proof