flffbas

Description: Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Hypothesis	flffbas.l	$⊢ L = Y filGen B$
	Assertion	flffbas	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \exists s \in B F [s] \subseteq o)))$

Proof

Step	Hyp	Ref	Expression
1		flffbas.l	$⊢ L = Y filGen B$
2		fgcl	$⊢ B \in fBas (Y) \to Y filGen B \in Fil (Y)$
3	1 2	eqeltrid	$⊢ B \in fBas (Y) \to L \in Fil (Y)$
4		isflf	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \exists t \in L F [t] \subseteq o)))$
5	3 4	syl3an2	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \exists t \in L F [t] \subseteq o)))$
6	1	eleq2i	$⊢ t \in L \leftrightarrow t \in (Y filGen B)$
7		elfg	$⊢ B \in fBas (Y) \to (t \in (Y filGen B) \leftrightarrow (t \subseteq Y \land \exists s \in B s \subseteq t))$
8	7	3ad2ant2	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (t \in (Y filGen B) \leftrightarrow (t \subseteq Y \land \exists s \in B s \subseteq t))$
9		sstr2	$⊢ F [s] \subseteq F [t] \to (F [t] \subseteq o \to F [s] \subseteq o)$
10		imass2	$⊢ s \subseteq t \to F [s] \subseteq F [t]$
11	9 10	syl11	$⊢ F [t] \subseteq o \to (s \subseteq t \to F [s] \subseteq o)$
12	11	adantl	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land F [t] \subseteq o) \to (s \subseteq t \to F [s] \subseteq o)$
13	12	reximdv	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land F [t] \subseteq o) \to (\exists s \in B s \subseteq t \to \exists s \in B F [s] \subseteq o)$
14	13	ex	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (F [t] \subseteq o \to (\exists s \in B s \subseteq t \to \exists s \in B F [s] \subseteq o))$
15	14	com23	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists s \in B s \subseteq t \to (F [t] \subseteq o \to \exists s \in B F [s] \subseteq o))$
16	15	adantld	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ((t \subseteq Y \land \exists s \in B s \subseteq t) \to (F [t] \subseteq o \to \exists s \in B F [s] \subseteq o))$
17	8 16	sylbid	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (t \in (Y filGen B) \to (F [t] \subseteq o \to \exists s \in B F [s] \subseteq o))$
18	17	adantr	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to (t \in (Y filGen B) \to (F [t] \subseteq o \to \exists s \in B F [s] \subseteq o))$
19	6 18	biimtrid	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to (t \in L \to (F [t] \subseteq o \to \exists s \in B F [s] \subseteq o))$
20	19	rexlimdv	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to (\exists t \in L F [t] \subseteq o \to \exists s \in B F [s] \subseteq o)$
21		ssfg	$⊢ B \in fBas (Y) \to B \subseteq Y filGen B$
22	21 1	sseqtrrdi	$⊢ B \in fBas (Y) \to B \subseteq L$
23	22	sselda	$⊢ (B \in fBas (Y) \land s \in B) \to s \in L$
24	23	3ad2antl2	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land s \in B) \to s \in L$
25	24	ad2ant2r	$⊢ (((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \land (s \in B \land F [s] \subseteq o)) \to s \in L$
26		simprr	$⊢ (((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \land (s \in B \land F [s] \subseteq o)) \to F [s] \subseteq o$
27		imaeq2	$⊢ t = s \to F [t] = F [s]$
28	27	sseq1d	$⊢ t = s \to (F [t] \subseteq o \leftrightarrow F [s] \subseteq o)$
29	28	rspcev	$⊢ (s \in L \land F [s] \subseteq o) \to \exists t \in L F [t] \subseteq o$
30	25 26 29	syl2anc	$⊢ (((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \land (s \in B \land F [s] \subseteq o)) \to \exists t \in L F [t] \subseteq o$
31	30	rexlimdvaa	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to (\exists s \in B F [s] \subseteq o \to \exists t \in L F [t] \subseteq o)$
32	20 31	impbid	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to (\exists t \in L F [t] \subseteq o \leftrightarrow \exists s \in B F [s] \subseteq o)$
33	32	imbi2d	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to ((A \in o \to \exists t \in L F [t] \subseteq o) \leftrightarrow (A \in o \to \exists s \in B F [s] \subseteq o))$
34	33	ralbidv	$⊢ ((J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall o \in J (A \in o \to \exists t \in L F [t] \subseteq o) \leftrightarrow \forall o \in J (A \in o \to \exists s \in B F [s] \subseteq o))$
35	34	pm5.32da	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ((A \in X \land \forall o \in J (A \in o \to \exists t \in L F [t] \subseteq o)) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \exists s \in B F [s] \subseteq o)))$
36	5 35	bitrd	$⊢ (J \in TopOn (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \exists s \in B F [s] \subseteq o)))$

Metamath Proof Explorer

Theorem flffbas

Proof