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	8	raleqdv	$⊢ ((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) \leftrightarrow \forall x \in ⋃ J F \in (J CnP K) (x))$
10	6 9	mpbird	$⊢ ((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)$
11	2 10	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))$
12		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$
13		cnvimass	$⊢ F^{-1} [y] \subseteq dom F$
14		fdm	$⊢ F : X ⟶ Y \to dom F = X$
15	14	adantl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to dom F = X$
16	13 15	sseqtrid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land y \in K) \land F : X ⟶ Y) \to F^{-1} [y] \subseteq X$
17		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))$
18	16 17	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))$
19		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)$
20		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$
21		ffn	$⊢ F : X ⟶ Y \to F Fn X$
22	21	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$
23		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]$
24		elpreima	$⊢ F Fn X \to (x \in F^{-1} [y] \leftrightarrow (x \in X \land F (x) \in y))$
25	24	simplbda	$⊢ (F Fn X \land x \in F^{-1} [y]) \to F (x) \in y$
26	22 23 25	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$
27		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)$
28	19 20 26 27	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)$
29		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$
30	29	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$
31		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)$
32		toponss	$⊢ (J \in TopOn (X) \land u \in J) \to u \subseteq X$
33	31 32	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$
34	29 14	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$
35	33 34	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$
36		funimass3	$⊢ (Fun F \land u \subseteq dom F) \to (F [u] \subseteq y \leftrightarrow u \subseteq F^{-1} [y])$
37	30 35 36	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])$
38	37	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]))$
39	38	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]))$
40	28 39	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])$
41	40	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]))$
42	41	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]))$
43	18 42	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]))$
44	43	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])$
45	44	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])$
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 \forall x \in X F \in (J CnP K) (x))) \land y \in K) \to J \in Top$
48		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]))$
49	47 48	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]))$
50	45 49	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$
51	50	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$
52	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))$
53	12 51 52	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)$
54	11 53	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