Metamath Proof Explorer

Theorem elflim2

Description: The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		flimval.1	$⊢ X = ⋃ J$
2		anass	$⊢ (((J \in Top \land F \in ⋃ ran Fil) \land F \subseteq 𝒫 X) \land (A \in X \land nei (J) (\{A\}) \subseteq F)) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil) \land (F \subseteq 𝒫 X \land (A \in X \land nei (J) (\{A\}) \subseteq F)))$
3		df-3an	$⊢ (J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 X) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil) \land F \subseteq 𝒫 X)$
4	3	anbi1i	$⊢ ((J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 X) \land (A \in X \land nei (J) (\{A\}) \subseteq F)) \leftrightarrow (((J \in Top \land F \in ⋃ ran Fil) \land F \subseteq 𝒫 X) \land (A \in X \land nei (J) (\{A\}) \subseteq F))$
5		df-flim	$⊢ fLim = (j \in Top, f \in ⋃ ran Fil ⟼ \{x \in ⋃ j \| (nei (j) (\{x\}) \subseteq f \land f \subseteq 𝒫 ⋃ j)\})$
6	5	elmpocl	$⊢ A \in (J fLim F) \to (J \in Top \land F \in ⋃ ran Fil)$
7	1	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)\}$
8	7	eleq2d	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to (A \in (J fLim F) \leftrightarrow A \in \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\})$
9		sneq	$⊢ x = A \to \{x\} = \{A\}$
10	9	fveq2d	$⊢ x = A \to nei (J) (\{x\}) = nei (J) (\{A\})$
11	10	sseq1d	$⊢ x = A \to (nei (J) (\{x\}) \subseteq F \leftrightarrow nei (J) (\{A\}) \subseteq F)$
12	11	anbi1d	$⊢ x = A \to ((nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X) \leftrightarrow (nei (J) (\{A\}) \subseteq F \land F \subseteq 𝒫 X))$
13	12	biancomd	$⊢ x = A \to ((nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X) \leftrightarrow (F \subseteq 𝒫 X \land nei (J) (\{A\}) \subseteq F))$
14	13	elrab	$⊢ A \in \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\} \leftrightarrow (A \in X \land (F \subseteq 𝒫 X \land nei (J) (\{A\}) \subseteq F))$
15		an12	$⊢ (A \in X \land (F \subseteq 𝒫 X \land nei (J) (\{A\}) \subseteq F)) \leftrightarrow (F \subseteq 𝒫 X \land (A \in X \land nei (J) (\{A\}) \subseteq F))$
16	14 15	bitri	$⊢ A \in \{x \in X \| (nei (J) (\{x\}) \subseteq F \land F \subseteq 𝒫 X)\} \leftrightarrow (F \subseteq 𝒫 X \land (A \in X \land nei (J) (\{A\}) \subseteq F))$
17	8 16	bitrdi	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to (A \in (J fLim F) \leftrightarrow (F \subseteq 𝒫 X \land (A \in X \land nei (J) (\{A\}) \subseteq F)))$
18	6 17	biadanii	$⊢ A \in (J fLim F) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil) \land (F \subseteq 𝒫 X \land (A \in X \land nei (J) (\{A\}) \subseteq F)))$
19	2 4 18	3bitr4ri	$⊢ A \in (J fLim F) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 X) \land (A \in X \land nei (J) (\{A\}) \subseteq F))$