Metamath Proof Explorer

Theorem flimval

Description: The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	flimval.1	$⊢ X = ⋃ J$
	Assertion	flimval	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to J fLim F = \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\}$

Proof

Step	Hyp	Ref	Expression
1		flimval.1	$⊢ X = ⋃ J$
2	1	topopn	$⊢ J \in Top \to X \in J$
3	2	adantr	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to X \in J$
4		rabexg	$⊢ X \in J \to \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\} \in V$
5	3 4	syl	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\} \in V$
6		simpl	$⊢ (j = J \land f = F) \to j = J$
7	6	unieqd	$⊢ (j = J \land f = F) \to ⋃ j = ⋃ J$
8	7 1	eqtr4di	$⊢ (j = J \land f = F) \to ⋃ j = X$
9	6	fveq2d	$⊢ (j = J \land f = F) \to nei (j) = nei (J)$
10	9	fveq1d	$⊢ (j = J \land f = F) \to nei (j) (\{x\}) = nei (J) (\{x\})$
11		simpr	$⊢ (j = J \land f = F) \to f = F$
12	10 11	sseq12d	$⊢ (j = J \land f = F) \to (nei (j) (\{x\}) \subseteq f \leftrightarrow nei (J) (\{x\}) \subseteq F)$
13	8	pweqd	$⊢ (j = J \land f = F) \to 𝒫 ⋃ j = 𝒫 X$
14	11 13	sseq12d	$⊢ (j = J \land f = F) \to (f \subseteq 𝒫 ⋃ j \leftrightarrow F \subseteq 𝒫 X)$
15	12 14	anbi12d	$⊢ (j = J \land f = F) \to ((nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j) \leftrightarrow (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X))$
16	8 15	rabeqbidv	$⊢ (j = J \land f = F) \to \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\} = \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\}$
17		df-flim	$⊢ fLim = (j \in Top, f \in ⋃ ran Fil ⟼ \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\})$
18	16 17	ovmpoga	$⊢ (J \in Top \land F \in ⋃ ran Fil \land \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\} \in V) \to J fLim F = \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\}$
19	5 18	mpd3an3	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to J fLim F = \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\}$