cncls

Description: Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	cncls	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x])))$

Proof

Step	Hyp	Ref	Expression
1		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Cn K)) \to F : X ⟶ Y$
2	1	3expia	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \to F : X ⟶ Y)$
3		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
4	3	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 X) \to x \subseteq X$
5		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
6	5	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 X) \to X = ⋃ J$
7	4 6	sseqtrd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 X) \to x \subseteq ⋃ J$
8		eqid	$⊢ ⋃ J = ⋃ J$
9	8	cnclsi	$⊢ (F \in (J Cn K) \land x \subseteq ⋃ J) \to F [cls (J) (x)] \subseteq cls (K) (F [x])$
10	9	expcom	$⊢ x \subseteq ⋃ J \to (F \in (J Cn K) \to F [cls (J) (x)] \subseteq cls (K) (F [x]))$
11	7 10	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 X) \to (F \in (J Cn K) \to F [cls (J) (x)] \subseteq cls (K) (F [x]))$
12	11	ralrimdva	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \to \forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x]))$
13	2 12	jcad	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \to (F : X ⟶ Y \land \forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x])))$
14		toponmax	$⊢ J \in TopOn (X) \to X \in J$
15	14	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to X \in J$
16		cnvimass	$⊢ F^{-1} [y] \subseteq dom F$
17		fdm	$⊢ F : X ⟶ Y \to dom F = X$
18	17	ad2antlr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to dom F = X$
19	16 18	sseqtrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to F^{-1} [y] \subseteq X$
20	15 19	sselpwd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to F^{-1} [y] \in 𝒫 X$
21		fveq2	$⊢ x = F^{-1} [y] \to cls (J) (x) = cls (J) (F^{-1} [y])$
22	21	imaeq2d	$⊢ x = F^{-1} [y] \to F [cls (J) (x)] = F [cls (J) (F^{-1} [y])]$
23		imaeq2	$⊢ x = F^{-1} [y] \to F [x] = F [F^{-1} [y]]$
24	23	fveq2d	$⊢ x = F^{-1} [y] \to cls (K) (F [x]) = cls (K) (F [F^{-1} [y]])$
25	22 24	sseq12d	$⊢ x = F^{-1} [y] \to (F [cls (J) (x)] \subseteq cls (K) (F [x]) \leftrightarrow F [cls (J) (F^{-1} [y])] \subseteq cls (K) (F [F^{-1} [y]]))$
26	25	rspcv	$⊢ F^{-1} [y] \in 𝒫 X \to (\forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x]) \to F [cls (J) (F^{-1} [y])] \subseteq cls (K) (F [F^{-1} [y]]))$
27	20 26	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to (\forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x]) \to F [cls (J) (F^{-1} [y])] \subseteq cls (K) (F [F^{-1} [y]]))$
28		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
29	28	ad3antlr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to K \in Top$
30		elpwi	$⊢ y \in 𝒫 Y \to y \subseteq Y$
31	30	adantl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to y \subseteq Y$
32		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
33	32	ad3antlr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to Y = ⋃ K$
34	31 33	sseqtrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to y \subseteq ⋃ K$
35		ffun	$⊢ F : X ⟶ Y \to Fun F$
36	35	ad2antlr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to Fun F$
37		funimacnv	$⊢ Fun F \to F [F^{-1} [y]] = y \cap ran F$
38	36 37	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to F [F^{-1} [y]] = y \cap ran F$
39		inss1	$⊢ y \cap ran F \subseteq y$
40	38 39	eqsstrdi	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to F [F^{-1} [y]] \subseteq y$
41		eqid	$⊢ ⋃ K = ⋃ K$
42	41	clsss	$⊢ (K \in Top \land y \subseteq ⋃ K \land F [F^{-1} [y]] \subseteq y) \to cls (K) (F [F^{-1} [y]]) \subseteq cls (K) (y)$
43	29 34 40 42	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to cls (K) (F [F^{-1} [y]]) \subseteq cls (K) (y)$
44		sstr2	$⊢ F [cls (J) (F^{-1} [y])] \subseteq cls (K) (F [F^{-1} [y]]) \to (cls (K) (F [F^{-1} [y]]) \subseteq cls (K) (y) \to F [cls (J) (F^{-1} [y])] \subseteq cls (K) (y))$
45	43 44	syl5com	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to (F [cls (J) (F^{-1} [y])] \subseteq cls (K) (F [F^{-1} [y]]) \to F [cls (J) (F^{-1} [y])] \subseteq cls (K) (y))$
46		topontop	$⊢ J \in TopOn (X) \to J \in Top$
47	46	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to J \in Top$
48	5	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to X = ⋃ J$
49	18 48	eqtrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to dom F = ⋃ J$
50	16 49	sseqtrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to F^{-1} [y] \subseteq ⋃ J$
51	8	clsss3	$⊢ (J \in Top \land F^{-1} [y] \subseteq ⋃ J) \to cls (J) (F^{-1} [y]) \subseteq ⋃ J$
52	47 50 51	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to cls (J) (F^{-1} [y]) \subseteq ⋃ J$
53	52 49	sseqtrrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to cls (J) (F^{-1} [y]) \subseteq dom F$
54		funimass3	$⊢ (Fun F \land cls (J) (F^{-1} [y]) \subseteq dom F) \to (F [cls (J) (F^{-1} [y])] \subseteq cls (K) (y) \leftrightarrow cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)])$
55	36 53 54	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to (F [cls (J) (F^{-1} [y])] \subseteq cls (K) (y) \leftrightarrow cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)])$
56	45 55	sylibd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to (F [cls (J) (F^{-1} [y])] \subseteq cls (K) (F [F^{-1} [y]]) \to cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)])$
57	27 56	syld	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land y \in 𝒫 Y) \to (\forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x]) \to cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)])$
58	57	ralrimdva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x]) \to \forall y \in 𝒫 Y cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)])$
59	58	imdistanda	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x])) \to (F : X ⟶ Y \land \forall y \in 𝒫 Y cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)]))$
60		cncls2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in 𝒫 Y cls (J) (F^{-1} [y]) \subseteq F^{-1} [cls (K) (y)]))$
61	59 60	sylibrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x])) \to F \in (J Cn K))$
62	13 61	impbid	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in 𝒫 X F [cls (J) (x)] \subseteq cls (K) (F [x])))$

Metamath Proof Explorer

Theorem cncls

Proof