cncnp

Description: A continuous function is continuous at all points. Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 15-May-2007) (Proof shortened by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	cncnp	$⊢ (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 \in (J CnP K) (x)))$

Proof

Step	Hyp	Ref	Expression
1		iscn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$
2	1	simprbda	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to F : X ⟶ Y$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	cncnpi	$⊢ (F \in (J Cn K) \land x \in ⋃ J) \to F \in (J CnP K) (x)$
5	4	ralrimiva	$⊢ F \in (J Cn K) \to \forall x \in ⋃ J F \in (J CnP K) (x)$
6	5	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to \forall x \in ⋃ J F \in (J CnP K) (x)$
7		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
8	7	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to X = ⋃ J$
9	6 8	raleqtrrdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to \forall x \in X F \in (J CnP K) (x)$
10	2 9	jca	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))$
11		simprl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \to F : X ⟶ Y$
12		cnvimass	$⊢ F^{-1} [y] \subseteq dom F$
13		fdm	$⊢ F : X ⟶ Y \to dom F = X$
14	13	adantl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to dom F = X$
15	12 14	sseqtrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to F^{-1} [y] \subseteq X$
16		ssralv	$⊢ F^{-1} [y] \subseteq X \to (\forall x \in X F \in (J CnP K) (x) \to \forall x \in F^{-1} [y] F \in (J CnP K) (x))$
17	15 16	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to (\forall x \in X F \in (J CnP K) (x) \to \forall x \in F^{-1} [y] F \in (J CnP K) (x))$
18		simprr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to F \in (J CnP K) (x)$
19		simpllr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to y \in K$
20		ffn	$⊢ F : X ⟶ Y \to F Fn X$
21	20	ad2antlr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to F Fn X$
22		simprl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to x \in F^{-1} [y]$
23		elpreima	$⊢ F Fn X \to (x \in F^{-1} [y] \leftrightarrow (x \in X \land F (x) \in y))$
24	23	simplbda	$⊢ (F Fn X \land x \in F^{-1} [y]) \to F (x) \in y$
25	21 22 24	syl2anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to F (x) \in y$
26		cnpimaex	$⊢ (F \in (J CnP K) (x) \land y \in K \land F (x) \in y) \to \exists u \in J (x \in u \land F [u] \subseteq y)$
27	18 19 25 26	syl3anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to \exists u \in J (x \in u \land F [u] \subseteq y)$
28		simpllr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to F : X ⟶ Y$
29	28	ffund	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to Fun F$
30		simp-4l	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to J \in TopOn (X)$
31		toponss	$⊢ (J \in TopOn (X) \land u \in J) \to u \subseteq X$
32	30 31	sylan	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to u \subseteq X$
33	28 13	syl	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to dom F = X$
34	32 33	sseqtrrd	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to u \subseteq dom F$
35		funimass3	$⊢ (Fun F \land u \subseteq dom F) \to (F [u] \subseteq y \leftrightarrow u \subseteq F^{-1} [y])$
36	29 34 35	syl2anc	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to (F [u] \subseteq y \leftrightarrow u \subseteq F^{-1} [y])$
37	36	anbi2d	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \land u \in J) \to ((x \in u \land F [u] \subseteq y) \leftrightarrow (x \in u \land u \subseteq F^{-1} [y]))$
38	37	rexbidva	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to (\exists u \in J (x \in u \land F [u] \subseteq y) \leftrightarrow \exists u \in J (x \in u \land u \subseteq F^{-1} [y]))$
39	27 38	mpbid	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land (x \in F^{-1} [y] \land F \in (J CnP K) (x))) \to \exists u \in J (x \in u \land u \subseteq F^{-1} [y])$
40	39	expr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \land x \in F^{-1} [y]) \to (F \in (J CnP K) (x) \to \exists u \in J (x \in u \land u \subseteq F^{-1} [y]))$
41	40	ralimdva	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to (\forall x \in F^{-1} [y] F \in (J CnP K) (x) \to \forall x \in F^{-1} [y] \exists u \in J (x \in u \land u \subseteq F^{-1} [y]))$
42	17 41	syld	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to (\forall x \in X F \in (J CnP K) (x) \to \forall x \in F^{-1} [y] \exists u \in J (x \in u \land u \subseteq F^{-1} [y]))$
43	42	impr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \to \forall x \in F^{-1} [y] \exists u \in J (x \in u \land u \subseteq F^{-1} [y])$
44	43	an32s	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \land y \in K) \to \forall x \in F^{-1} [y] \exists u \in J (x \in u \land u \subseteq F^{-1} [y])$
45		topontop	$⊢ J \in TopOn (X) \to J \in Top$
46	45	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \land y \in K) \to J \in Top$
47		eltop2	$⊢ J \in Top \to (F^{-1} [y] \in J \leftrightarrow \forall x \in F^{-1} [y] \exists u \in J (x \in u \land u \subseteq F^{-1} [y]))$
48	46 47	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \land y \in K) \to (F^{-1} [y] \in J \leftrightarrow \forall x \in F^{-1} [y] \exists u \in J (x \in u \land u \subseteq F^{-1} [y]))$
49	44 48	mpbird	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \land y \in K) \to F^{-1} [y] \in J$
50	49	ralrimiva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \to \forall y \in K F^{-1} [y] \in J$
51	1	adantr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in K F^{-1} [y] \in J))$
52	11 50 51	mpbir2and	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x))) \to F \in (J Cn K)$
53	10 52	impbida	$⊢ (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 \in (J CnP K) (x)))$

Metamath Proof Explorer

Theorem cncnp

Proof