cncnp2

Description: A continuous function is continuous at all points. Theorem 7.2(g) of Munkres p. 107. (Contributed by Raph Levien, 20-Nov-2006) (Proof shortened by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	cncnp.1	$⊢ X = ⋃ J$
	cncnp.2	$⊢ Y = ⋃ K$
Assertion	cncnp2	$⊢ X \neq \emptyset \to (F \in (J Cn K) \leftrightarrow \forall x \in X F \in (J CnP K) (x))$

Proof

Step	Hyp	Ref	Expression
1		cncnp.1	$⊢ X = ⋃ J$
2		cncnp.2	$⊢ Y = ⋃ K$
3		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
4	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
5	3 4	sylib	$⊢ F \in (J Cn K) \to J \in TopOn (X)$
6		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
7	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
8	6 7	sylib	$⊢ F \in (J Cn K) \to K \in TopOn (Y)$
9	1 2	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ Y$
10	5 8 9	jca31	$⊢ F \in (J Cn K) \to ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y)$
11	10	adantl	$⊢ (X \neq \emptyset \land F \in (J Cn K)) \to ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y)$
12		r19.2z	$⊢ (X \neq \emptyset \land \forall x \in X F \in (J CnP K) (x)) \to \exists x \in X F \in (J CnP K) (x)$
13		cnptop1	$⊢ F \in (J CnP K) (x) \to J \in Top$
14	13 4	sylib	$⊢ F \in (J CnP K) (x) \to J \in TopOn (X)$
15		cnptop2	$⊢ F \in (J CnP K) (x) \to K \in Top$
16	15 7	sylib	$⊢ F \in (J CnP K) (x) \to K \in TopOn (Y)$
17	1 2	cnpf	$⊢ F \in (J CnP K) (x) \to F : X ⟶ Y$
18	14 16 17	jca31	$⊢ F \in (J CnP K) (x) \to ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y)$
19	18	rexlimivw	$⊢ \exists x \in X F \in (J CnP K) (x) \to ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y)$
20	12 19	syl	$⊢ (X \neq \emptyset \land \forall x \in X F \in (J CnP K) (x)) \to ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y)$
21		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)))$
22	21	baibd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (F \in (J Cn K) \leftrightarrow \forall x \in X F \in (J CnP K) (x))$
23	11 20 22	pm5.21nd	$⊢ X \neq \emptyset \to (F \in (J Cn K) \leftrightarrow \forall x \in X F \in (J CnP K) (x))$

Metamath Proof Explorer

Theorem cncnp2

Proof