cnntr

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

		Ref	Expression
	Assertion	cnntr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in 𝒫 Y F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [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	cnntri	$⊢ (F \in (J Cn K) \land x \subseteq ⋃ K) \to F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])$
10	9	expcom	$⊢ x \subseteq ⋃ K \to (F \in (J Cn K) \to F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [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 F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x]))$
12	11	ralrimdva	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \to \forall x \in 𝒫 Y F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [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 F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])))$
14		toponss	$⊢ (K \in TopOn (Y) \land x \in K) \to x \subseteq Y$
15		velpw	$⊢ x \in 𝒫 Y \leftrightarrow x \subseteq Y$
16	14 15	sylibr	$⊢ (K \in TopOn (Y) \land x \in K) \to x \in 𝒫 Y$
17	16	ex	$⊢ K \in TopOn (Y) \to (x \in K \to x \in 𝒫 Y)$
18	17	ad2antlr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (x \in 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 F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])) \to (x \in K \to F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])))$
20		topontop	$⊢ J \in TopOn (X) \to J \in Top$
21	20	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to J \in Top$
22		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
23		fdm	$⊢ F : X ⟶ Y \to dom F = X$
24	23	ad2antlr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to dom F = X$
25		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
26	25	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to X = ⋃ J$
27	24 26	eqtrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to dom F = ⋃ J$
28	22 27	sseqtrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to F^{-1} [x] \subseteq ⋃ J$
29		eqid	$⊢ ⋃ J = ⋃ J$
30	29	ntrss2	$⊢ (J \in Top \land F^{-1} [x] \subseteq ⋃ J) \to int (J) (F^{-1} [x]) \subseteq F^{-1} [x]$
31	21 28 30	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to int (J) (F^{-1} [x]) \subseteq F^{-1} [x]$
32		eqss	$⊢ int (J) (F^{-1} [x]) = F^{-1} [x] \leftrightarrow (int (J) (F^{-1} [x]) \subseteq F^{-1} [x] \land F^{-1} [x] \subseteq int (J) (F^{-1} [x]))$
33	32	baib	$⊢ int (J) (F^{-1} [x]) \subseteq F^{-1} [x] \to (int (J) (F^{-1} [x]) = F^{-1} [x] \leftrightarrow F^{-1} [x] \subseteq int (J) (F^{-1} [x]))$
34	31 33	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to (int (J) (F^{-1} [x]) = F^{-1} [x] \leftrightarrow F^{-1} [x] \subseteq int (J) (F^{-1} [x]))$
35	29	isopn3	$⊢ (J \in Top \land F^{-1} [x] \subseteq ⋃ J) \to (F^{-1} [x] \in J \leftrightarrow int (J) (F^{-1} [x]) = F^{-1} [x])$
36	21 28 35	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to (F^{-1} [x] \in J \leftrightarrow int (J) (F^{-1} [x]) = F^{-1} [x])$
37		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
38	37	ad3antlr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to K \in Top$
39		isopn3i	$⊢ (K \in Top \land x \in K) \to int (K) (x) = x$
40	38 39	sylancom	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to int (K) (x) = x$
41	40	imaeq2d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to F^{-1} [int (K) (x)] = F^{-1} [x]$
42	41	sseq1d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to (F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x]) \leftrightarrow F^{-1} [x] \subseteq int (J) (F^{-1} [x]))$
43	34 36 42	3bitr4rd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land x \in K) \to (F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x]) \leftrightarrow F^{-1} [x] \in J)$
44	43	pm5.74da	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to ((x \in K \to F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])) \leftrightarrow (x \in K \to F^{-1} [x] \in J))$
45	19 44	sylibd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to ((x \in 𝒫 Y \to F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])) \to (x \in K \to F^{-1} [x] \in J))$
46	45	ralimdv2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall x \in 𝒫 Y F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x]) \to \forall x \in K F^{-1} [x] \in J)$
47	46	imdistanda	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in 𝒫 Y F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])) \to (F : X ⟶ Y \land \forall x \in K F^{-1} [x] \in J))$
48		iscn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in K F^{-1} [x] \in J))$
49	47 48	sylibrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in 𝒫 Y F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])) \to F \in (J Cn K))$
50	13 49	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 F^{-1} [int (K) (x)] \subseteq int (J) (F^{-1} [x])))$

Metamath Proof Explorer

Theorem cnntr

Proof