cncls2

Description: Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	cncls2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (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 𝒫 Y \to x \subseteq Y$
4	3	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 Y) \to x \subseteq Y$
5		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
6	5	ad2antlr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 Y) \to Y = ⋃ K$
7	4 6	sseqtrd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 Y) \to x \subseteq ⋃ K$
8		eqid	$⊢ ⋃ K = ⋃ K$
9	8	cncls2i	$⊢ (F \in (J Cn K) \land x \subseteq ⋃ K) \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]$
10	9	expcom	$⊢ x \subseteq ⋃ K \to (F \in (J Cn K) \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)])$
11	7 10	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land x \in 𝒫 Y) \to (F \in (J Cn K) \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)])$
12	11	ralrimdva	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \to \forall x \in 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (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 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]))$
14	8	cldss2	$⊢ Clsd (K) \subseteq 𝒫 ⋃ K$
15	5	ad2antlr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to Y = ⋃ K$
16	15	pweqd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to 𝒫 Y = 𝒫 ⋃ K$
17	14 16	sseqtrrid	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to Clsd (K) \subseteq 𝒫 Y$
18	17	sseld	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (x \in Clsd (K) \to x \in 𝒫 Y)$
19	18	imim1d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to ((x \in 𝒫 Y \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]) \to (x \in Clsd (K) \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]))$
20		cldcls	$⊢ x \in Clsd (K) \to cls (K) (x) = x$
21	20	ad2antll	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to cls (K) (x) = x$
22	21	imaeq2d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to F^{-1} [cls (K) (x)] = F^{-1} [x]$
23	22	sseq2d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to (cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)] \leftrightarrow cls (J) (F^{-1} [x]) \subseteq F^{-1} [x])$
24		topontop	$⊢ J \in TopOn (X) \to J \in Top$
25	24	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to J \in Top$
26		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
27		fdm	$⊢ F : X ⟶ Y \to dom F = X$
28	27	ad2antrl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to dom F = X$
29		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
30	29	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to X = ⋃ J$
31	28 30	eqtrd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to dom F = ⋃ J$
32	26 31	sseqtrid	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to F^{-1} [x] \subseteq ⋃ J$
33		eqid	$⊢ ⋃ J = ⋃ J$
34	33	iscld4	$⊢ (J \in Top \land F^{-1} [x] \subseteq ⋃ J) \to (F^{-1} [x] \in Clsd (J) \leftrightarrow cls (J) (F^{-1} [x]) \subseteq F^{-1} [x])$
35	25 32 34	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to (F^{-1} [x] \in Clsd (J) \leftrightarrow cls (J) (F^{-1} [x]) \subseteq F^{-1} [x])$
36	23 35	bitr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land x \in Clsd (K))) \to (cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)] \leftrightarrow F^{-1} [x] \in Clsd (J))$
37	36	expr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (x \in Clsd (K) \to (cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)] \leftrightarrow F^{-1} [x] \in Clsd (J)))$
38	37	pm5.74d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to ((x \in Clsd (K) \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]) \leftrightarrow (x \in Clsd (K) \to F^{-1} [x] \in Clsd (J)))$
39	19 38	sylibd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to ((x \in 𝒫 Y \to cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]) \to (x \in Clsd (K) \to F^{-1} [x] \in Clsd (J)))$
40	39	ralimdv2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall x \in 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)] \to \forall x \in Clsd (K) F^{-1} [x] \in Clsd (J))$
41	40	imdistanda	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]) \to (F : X ⟶ Y \land \forall x \in Clsd (K) F^{-1} [x] \in Clsd (J)))$
42		iscncl	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in Clsd (K) F^{-1} [x] \in Clsd (J)))$
43	41 42	sylibrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]) \to F \in (J Cn K))$
44	13 43	impbid	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in 𝒫 Y cls (J) (F^{-1} [x]) \subseteq F^{-1} [cls (K) (x)]))$

Metamath Proof Explorer

Theorem cncls2

Proof