tgcnp

Description: The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	tgcn.1	$⊢ φ \to J \in TopOn (X)$
	tgcn.3	$⊢ φ \to K = topGen (B)$
	tgcn.4	$⊢ φ \to K \in TopOn (Y)$
	tgcnp.5	$⊢ φ \to P \in X$
Assertion	tgcnp	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$

Proof

Step	Hyp	Ref	Expression
1		tgcn.1	$⊢ φ \to J \in TopOn (X)$
2		tgcn.3	$⊢ φ \to K = topGen (B)$
3		tgcn.4	$⊢ φ \to K \in TopOn (Y)$
4		tgcnp.5	$⊢ φ \to P \in X$
5		iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
6	1 3 4 5	syl3anc	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
7		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
8	3 7	syl	$⊢ φ \to K \in Top$
9	2 8	eqeltrrd	$⊢ φ \to topGen (B) \in Top$
10		tgclb	$⊢ B \in TopBases \leftrightarrow topGen (B) \in Top$
11	9 10	sylibr	$⊢ φ \to B \in TopBases$
12		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
13	11 12	syl	$⊢ φ \to B \subseteq topGen (B)$
14	13 2	sseqtrrd	$⊢ φ \to B \subseteq K$
15		ssralv	$⊢ B \subseteq K \to (\forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)))$
16	14 15	syl	$⊢ φ \to (\forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)))$
17	16	anim2d	$⊢ φ \to ((F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))) \to (F : X ⟶ Y \land \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
18	6 17	sylbid	$⊢ φ \to (F \in (J CnP K) (P) \to (F : X ⟶ Y \land \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
19	2	eleq2d	$⊢ φ \to (z \in K \leftrightarrow z \in topGen (B))$
20	19	biimpa	$⊢ (φ \land z \in K) \to z \in topGen (B)$
21		tg2	$⊢ (z \in topGen (B) \land F (P) \in z) \to \exists y \in B (F (P) \in y \land y \subseteq z)$
22		r19.29	$⊢ (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \land \exists y \in B (F (P) \in y \land y \subseteq z)) \to \exists y \in B ((F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \land (F (P) \in y \land y \subseteq z))$
23		sstr	$⊢ (F [x] \subseteq y \land y \subseteq z) \to F [x] \subseteq z$
24	23	expcom	$⊢ y \subseteq z \to (F [x] \subseteq y \to F [x] \subseteq z)$
25	24	anim2d	$⊢ y \subseteq z \to ((P \in x \land F [x] \subseteq y) \to (P \in x \land F [x] \subseteq z))$
26	25	reximdv	$⊢ y \subseteq z \to (\exists x \in J (P \in x \land F [x] \subseteq y) \to \exists x \in J (P \in x \land F [x] \subseteq z))$
27	26	com12	$⊢ \exists x \in J (P \in x \land F [x] \subseteq y) \to (y \subseteq z \to \exists x \in J (P \in x \land F [x] \subseteq z))$
28	27	imim2i	$⊢ (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to (F (P) \in y \to (y \subseteq z \to \exists x \in J (P \in x \land F [x] \subseteq z)))$
29	28	imp32	$⊢ ((F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \land (F (P) \in y \land y \subseteq z)) \to \exists x \in J (P \in x \land F [x] \subseteq z)$
30	29	rexlimivw	$⊢ \exists y \in B ((F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \land (F (P) \in y \land y \subseteq z)) \to \exists x \in J (P \in x \land F [x] \subseteq z)$
31	22 30	syl	$⊢ (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \land \exists y \in B (F (P) \in y \land y \subseteq z)) \to \exists x \in J (P \in x \land F [x] \subseteq z)$
32	31	expcom	$⊢ \exists y \in B (F (P) \in y \land y \subseteq z) \to (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to \exists x \in J (P \in x \land F [x] \subseteq z))$
33	21 32	syl	$⊢ (z \in topGen (B) \land F (P) \in z) \to (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to \exists x \in J (P \in x \land F [x] \subseteq z))$
34	33	ex	$⊢ z \in topGen (B) \to (F (P) \in z \to (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to \exists x \in J (P \in x \land F [x] \subseteq z)))$
35	34	com23	$⊢ z \in topGen (B) \to (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to (F (P) \in z \to \exists x \in J (P \in x \land F [x] \subseteq z)))$
36	20 35	syl	$⊢ (φ \land z \in K) \to (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to (F (P) \in z \to \exists x \in J (P \in x \land F [x] \subseteq z)))$
37	36	ralrimdva	$⊢ φ \to (\forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to \forall z \in K (F (P) \in z \to \exists x \in J (P \in x \land F [x] \subseteq z)))$
38	37	anim2d	$⊢ φ \to ((F : X ⟶ Y \land \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))) \to (F : X ⟶ Y \land \forall z \in K (F (P) \in z \to \exists x \in J (P \in x \land F [x] \subseteq z))))$
39		iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall z \in K (F (P) \in z \to \exists x \in J (P \in x \land F [x] \subseteq z))))$
40	1 3 4 39	syl3anc	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall z \in K (F (P) \in z \to \exists x \in J (P \in x \land F [x] \subseteq z))))$
41	38 40	sylibrd	$⊢ φ \to ((F : X ⟶ Y \land \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))) \to F \in (J CnP K) (P))$
42	18 41	impbid	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in B (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$

Metamath Proof Explorer

Theorem tgcnp

Proof