flftg

Description: Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015)

		Ref	Expression
	Hypothesis	flftg.l	$⊢ J = topGen (B)$
	Assertion	flftg	$⊢ (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 B (A \in o \to \exists s \in L F [s] \subseteq o)))$

Proof

Step	Hyp	Ref	Expression
1		flftg.l	$⊢ J = topGen (B)$
2		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 u \in J (A \in u \to \exists s \in L F [s] \subseteq u)))$
3	1	raleqi	$⊢ \forall u \in J (A \in u \to \exists s \in L F [s] \subseteq u) \leftrightarrow \forall u \in topGen (B) (A \in u \to \exists s \in L F [s] \subseteq u)$
4		simpl1	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to J \in TopOn (X)$
5		topontop	$⊢ J \in TopOn (X) \to J \in Top$
6	4 5	syl	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to J \in Top$
7	1 6	eqeltrrid	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to topGen (B) \in Top$
8		tgclb	$⊢ B \in TopBases \leftrightarrow topGen (B) \in Top$
9	7 8	sylibr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to B \in TopBases$
10		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
11		eleq2w	$⊢ u = o \to (A \in u \leftrightarrow A \in o)$
12		sseq2	$⊢ u = o \to (F [s] \subseteq u \leftrightarrow F [s] \subseteq o)$
13	12	rexbidv	$⊢ u = o \to (\exists s \in L F [s] \subseteq u \leftrightarrow \exists s \in L F [s] \subseteq o)$
14	11 13	imbi12d	$⊢ u = o \to ((A \in u \to \exists s \in L F [s] \subseteq u) \leftrightarrow (A \in o \to \exists s \in L F [s] \subseteq o))$
15	14	cbvralvw	$⊢ \forall u \in topGen (B) (A \in u \to \exists s \in L F [s] \subseteq u) \leftrightarrow \forall o \in topGen (B) (A \in o \to \exists s \in L F [s] \subseteq o)$
16		ssralv	$⊢ B \subseteq topGen (B) \to (\forall o \in topGen (B) (A \in o \to \exists s \in L F [s] \subseteq o) \to \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o))$
17	15 16	biimtrid	$⊢ B \subseteq topGen (B) \to (\forall u \in topGen (B) (A \in u \to \exists s \in L F [s] \subseteq u) \to \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o))$
18	9 10 17	3syl	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall u \in topGen (B) (A \in u \to \exists s \in L F [s] \subseteq u) \to \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o))$
19		tg2	$⊢ (u \in topGen (B) \land A \in u) \to \exists o \in B (A \in o \land o \subseteq u)$
20		r19.29	$⊢ (\forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o) \land \exists o \in B (A \in o \land o \subseteq u)) \to \exists o \in B ((A \in o \to \exists s \in L F [s] \subseteq o) \land (A \in o \land o \subseteq u))$
21		simpl	$⊢ (A \in o \land o \subseteq u) \to A \in o$
22		simpr	$⊢ (A \in o \land o \subseteq u) \to o \subseteq u$
23		sstr2	$⊢ F [s] \subseteq o \to (o \subseteq u \to F [s] \subseteq u)$
24	22 23	syl5com	$⊢ (A \in o \land o \subseteq u) \to (F [s] \subseteq o \to F [s] \subseteq u)$
25	24	reximdv	$⊢ (A \in o \land o \subseteq u) \to (\exists s \in L F [s] \subseteq o \to \exists s \in L F [s] \subseteq u)$
26	21 25	embantd	$⊢ (A \in o \land o \subseteq u) \to ((A \in o \to \exists s \in L F [s] \subseteq o) \to \exists s \in L F [s] \subseteq u)$
27	26	impcom	$⊢ ((A \in o \to \exists s \in L F [s] \subseteq o) \land (A \in o \land o \subseteq u)) \to \exists s \in L F [s] \subseteq u$
28	27	rexlimivw	$⊢ \exists o \in B ((A \in o \to \exists s \in L F [s] \subseteq o) \land (A \in o \land o \subseteq u)) \to \exists s \in L F [s] \subseteq u$
29	20 28	syl	$⊢ (\forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o) \land \exists o \in B (A \in o \land o \subseteq u)) \to \exists s \in L F [s] \subseteq u$
30	29	ex	$⊢ \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o) \to (\exists o \in B (A \in o \land o \subseteq u) \to \exists s \in L F [s] \subseteq u)$
31	19 30	syl5	$⊢ \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o) \to ((u \in topGen (B) \land A \in u) \to \exists s \in L F [s] \subseteq u)$
32	31	expdimp	$⊢ (\forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o) \land u \in topGen (B)) \to (A \in u \to \exists s \in L F [s] \subseteq u)$
33	32	ralrimiva	$⊢ \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o) \to \forall u \in topGen (B) (A \in u \to \exists s \in L F [s] \subseteq u)$
34	18 33	impbid1	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall u \in topGen (B) (A \in u \to \exists s \in L F [s] \subseteq u) \leftrightarrow \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o))$
35	3 34	bitrid	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in X) \to (\forall u \in J (A \in u \to \exists s \in L F [s] \subseteq u) \leftrightarrow \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o))$
36	35	pm5.32da	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to ((A \in X \land \forall u \in J (A \in u \to \exists s \in L F [s] \subseteq u)) \leftrightarrow (A \in X \land \forall o \in B (A \in o \to \exists s \in L F [s] \subseteq o)))$
37	2 36	bitrd	$⊢ (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 B (A \in o \to \exists s \in L F [s] \subseteq o)))$

Metamath Proof Explorer

Theorem flftg

Proof