cncnpi

Description: A continuous function is continuous at all points. One direction of 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
	Hypothesis	cnsscnp.1	$⊢ X = ⋃ J$
	Assertion	cncnpi	$⊢ (F \in (J Cn K) \land A \in X) \to F \in (J CnP K) (A)$

Proof

Step	Hyp	Ref	Expression
1		cnsscnp.1	$⊢ X = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ ⋃ K$
4	3	adantr	$⊢ (F \in (J Cn K) \land A \in X) \to F : X ⟶ ⋃ K$
5		cnima	$⊢ (F \in (J Cn K) \land y \in K) \to F^{-1} [y] \in J$
6	5	ad2ant2r	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to F^{-1} [y] \in J$
7		simpr	$⊢ (F \in (J Cn K) \land A \in X) \to A \in X$
8	7	adantr	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to A \in X$
9		simprr	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to F (A) \in y$
10	3	ad2antrr	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to F : X ⟶ ⋃ K$
11		ffn	$⊢ F : X ⟶ ⋃ K \to F Fn X$
12		elpreima	$⊢ F Fn X \to (A \in F^{-1} [y] \leftrightarrow (A \in X \land F (A) \in y))$
13	10 11 12	3syl	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to (A \in F^{-1} [y] \leftrightarrow (A \in X \land F (A) \in y))$
14	8 9 13	mpbir2and	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to A \in F^{-1} [y]$
15		eqimss	$⊢ x = F^{-1} [y] \to x \subseteq F^{-1} [y]$
16	15	biantrud	$⊢ x = F^{-1} [y] \to (A \in x \leftrightarrow (A \in x \land x \subseteq F^{-1} [y]))$
17		eleq2	$⊢ x = F^{-1} [y] \to (A \in x \leftrightarrow A \in F^{-1} [y])$
18	16 17	bitr3d	$⊢ x = F^{-1} [y] \to ((A \in x \land x \subseteq F^{-1} [y]) \leftrightarrow A \in F^{-1} [y])$
19	18	rspcev	$⊢ (F^{-1} [y] \in J \land A \in F^{-1} [y]) \to \exists x \in J (A \in x \land x \subseteq F^{-1} [y])$
20	6 14 19	syl2anc	$⊢ ((F \in (J Cn K) \land A \in X) \land (y \in K \land F (A) \in y)) \to \exists x \in J (A \in x \land x \subseteq F^{-1} [y])$
21	20	expr	$⊢ ((F \in (J Cn K) \land A \in X) \land y \in K) \to (F (A) \in y \to \exists x \in J (A \in x \land x \subseteq F^{-1} [y]))$
22	21	ralrimiva	$⊢ (F \in (J Cn K) \land A \in X) \to \forall y \in K (F (A) \in y \to \exists x \in J (A \in x \land x \subseteq F^{-1} [y]))$
23		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
24	23	adantr	$⊢ (F \in (J Cn K) \land A \in X) \to J \in Top$
25	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
26	24 25	sylib	$⊢ (F \in (J Cn K) \land A \in X) \to J \in TopOn (X)$
27		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
28	27	adantr	$⊢ (F \in (J Cn K) \land A \in X) \to K \in Top$
29	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
30	28 29	sylib	$⊢ (F \in (J Cn K) \land A \in X) \to K \in TopOn (⋃ K)$
31		iscnp3	$⊢ (J \in TopOn (X) \land K \in TopOn (⋃ K) \land A \in X) \to (F \in (J CnP K) (A) \leftrightarrow (F : X ⟶ ⋃ K \land \forall y \in K (F (A) \in y \to \exists x \in J (A \in x \land x \subseteq F^{-1} [y]))))$
32	26 30 7 31	syl3anc	$⊢ (F \in (J Cn K) \land A \in X) \to (F \in (J CnP K) (A) \leftrightarrow (F : X ⟶ ⋃ K \land \forall y \in K (F (A) \in y \to \exists x \in J (A \in x \land x \subseteq F^{-1} [y]))))$
33	4 22 32	mpbir2and	$⊢ (F \in (J Cn K) \land A \in X) \to F \in (J CnP K) (A)$

Metamath Proof Explorer

Theorem cncnpi

Proof