subbascn

Description: The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	subbascn.1	$⊢ φ \to J \in TopOn (X)$
	subbascn.2	$⊢ φ \to B \in V$
	subbascn.3	$⊢ φ \to K = topGen (fi (B))$
	subbascn.4	$⊢ φ \to K \in TopOn (Y)$
Assertion	subbascn	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in B F^{-1} [y] \in J))$

Proof

Step	Hyp	Ref	Expression
1		subbascn.1	$⊢ φ \to J \in TopOn (X)$
2		subbascn.2	$⊢ φ \to B \in V$
3		subbascn.3	$⊢ φ \to K = topGen (fi (B))$
4		subbascn.4	$⊢ φ \to K \in TopOn (Y)$
5	1 3 4	tgcn	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in fi (B) F^{-1} [y] \in J))$
6	2	adantr	$⊢ (φ \land F : X ⟶ Y) \to B \in V$
7		ssfii	$⊢ B \in V \to B \subseteq fi (B)$
8		ssralv	$⊢ B \subseteq fi (B) \to (\forall y \in fi (B) F^{-1} [y] \in J \to \forall y \in B F^{-1} [y] \in J)$
9	6 7 8	3syl	$⊢ (φ \land F : X ⟶ Y) \to (\forall y \in fi (B) F^{-1} [y] \in J \to \forall y \in B F^{-1} [y] \in J)$
10		vex	$⊢ x \in V$
11		elfi	$⊢ (x \in V \land B \in V) \to (x \in fi (B) \leftrightarrow \exists z \in (𝒫 B \cap Fin) x = ⋂ z)$
12	10 6 11	sylancr	$⊢ (φ \land F : X ⟶ Y) \to (x \in fi (B) \leftrightarrow \exists z \in (𝒫 B \cap Fin) x = ⋂ z)$
13		simpr2	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to x = ⋂ z$
14	13	imaeq2d	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to F^{-1} [x] = F^{-1} [⋂ z]$
15		ffun	$⊢ F : X ⟶ Y \to Fun F$
16	15	ad2antlr	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to Fun F$
17	13 10	eqeltrrdi	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to ⋂ z \in V$
18		intex	$⊢ z \neq \emptyset \leftrightarrow ⋂ z \in V$
19	17 18	sylibr	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to z \neq \emptyset$
20		intpreima	$⊢ (Fun F \land z \neq \emptyset) \to F^{-1} [⋂ z] = ⋂_{y \in z} F^{-1} [y]$
21	16 19 20	syl2anc	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to F^{-1} [⋂ z] = ⋂_{y \in z} F^{-1} [y]$
22	14 21	eqtrd	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to F^{-1} [x] = ⋂_{y \in z} F^{-1} [y]$
23		topontop	$⊢ J \in TopOn (X) \to J \in Top$
24	1 23	syl	$⊢ φ \to J \in Top$
25	24	ad2antrr	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to J \in Top$
26		simpr1	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to z \in (𝒫 B \cap Fin)$
27	26	elin2d	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to z \in Fin$
28	26	elin1d	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to z \in 𝒫 B$
29	28	elpwid	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to z \subseteq B$
30		simpr3	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to \forall y \in B F^{-1} [y] \in J$
31		ssralv	$⊢ z \subseteq B \to (\forall y \in B F^{-1} [y] \in J \to \forall y \in z F^{-1} [y] \in J)$
32	29 30 31	sylc	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to \forall y \in z F^{-1} [y] \in J$
33		iinopn	$⊢ (J \in Top \land (z \in Fin \land z \neq \emptyset \land \forall y \in z F^{-1} [y] \in J)) \to ⋂_{y \in z} F^{-1} [y] \in J$
34	25 27 19 32 33	syl13anc	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to ⋂_{y \in z} F^{-1} [y] \in J$
35	22 34	eqeltrd	$⊢ ((φ \land F : X ⟶ Y) \land (z \in (𝒫 B \cap Fin) \land x = ⋂ z \land \forall y \in B F^{-1} [y] \in J)) \to F^{-1} [x] \in J$
36	35	3exp2	$⊢ (φ \land F : X ⟶ Y) \to (z \in (𝒫 B \cap Fin) \to (x = ⋂ z \to (\forall y \in B F^{-1} [y] \in J \to F^{-1} [x] \in J)))$
37	36	rexlimdv	$⊢ (φ \land F : X ⟶ Y) \to (\exists z \in (𝒫 B \cap Fin) x = ⋂ z \to (\forall y \in B F^{-1} [y] \in J \to F^{-1} [x] \in J))$
38	12 37	sylbid	$⊢ (φ \land F : X ⟶ Y) \to (x \in fi (B) \to (\forall y \in B F^{-1} [y] \in J \to F^{-1} [x] \in J))$
39	38	com23	$⊢ (φ \land F : X ⟶ Y) \to (\forall y \in B F^{-1} [y] \in J \to (x \in fi (B) \to F^{-1} [x] \in J))$
40	39	ralrimdv	$⊢ (φ \land F : X ⟶ Y) \to (\forall y \in B F^{-1} [y] \in J \to \forall x \in fi (B) F^{-1} [x] \in J)$
41		imaeq2	$⊢ y = x \to F^{-1} [y] = F^{-1} [x]$
42	41	eleq1d	$⊢ y = x \to (F^{-1} [y] \in J \leftrightarrow F^{-1} [x] \in J)$
43	42	cbvralvw	$⊢ \forall y \in fi (B) F^{-1} [y] \in J \leftrightarrow \forall x \in fi (B) F^{-1} [x] \in J$
44	40 43	syl6ibr	$⊢ (φ \land F : X ⟶ Y) \to (\forall y \in B F^{-1} [y] \in J \to \forall y \in fi (B) F^{-1} [y] \in J)$
45	9 44	impbid	$⊢ (φ \land F : X ⟶ Y) \to (\forall y \in fi (B) F^{-1} [y] \in J \leftrightarrow \forall y \in B F^{-1} [y] \in J)$
46	45	pm5.32da	$⊢ φ \to ((F : X ⟶ Y \land \forall y \in fi (B) F^{-1} [y] \in J) \leftrightarrow (F : X ⟶ Y \land \forall y \in B F^{-1} [y] \in J))$
47	5 46	bitrd	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in B F^{-1} [y] \in J))$

Metamath Proof Explorer

Theorem subbascn

Proof