cnpimaex

Description: Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006)

		Ref	Expression
	Assertion	cnpimaex	$⊢ (F \in (J CnP K) (P) \land A \in K \land F (P) \in A) \to \exists x \in J (P \in x \land F [x] \subseteq A)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	iscnp2	$⊢ F \in (J CnP K) (P) \leftrightarrow ((J \in Top \land K \in Top \land P \in ⋃ J) \land (F : ⋃ J ⟶ ⋃ K \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
4	3	simprbi	$⊢ F \in (J CnP K) (P) \to (F : ⋃ J ⟶ ⋃ K \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)))$
5		eleq2	$⊢ y = A \to (F (P) \in y \leftrightarrow F (P) \in A)$
6		sseq2	$⊢ y = A \to (F [x] \subseteq y \leftrightarrow F [x] \subseteq A)$
7	6	anbi2d	$⊢ y = A \to ((P \in x \land F [x] \subseteq y) \leftrightarrow (P \in x \land F [x] \subseteq A))$
8	7	rexbidv	$⊢ y = A \to (\exists x \in J (P \in x \land F [x] \subseteq y) \leftrightarrow \exists x \in J (P \in x \land F [x] \subseteq A))$
9	5 8	imbi12d	$⊢ y = A \to ((F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \leftrightarrow (F (P) \in A \to \exists x \in J (P \in x \land F [x] \subseteq A)))$
10	9	rspccv	$⊢ \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \to (A \in K \to (F (P) \in A \to \exists x \in J (P \in x \land F [x] \subseteq A)))$
11	4 10	simpl2im	$⊢ F \in (J CnP K) (P) \to (A \in K \to (F (P) \in A \to \exists x \in J (P \in x \land F [x] \subseteq A)))$
12	11	3imp	$⊢ (F \in (J CnP K) (P) \land A \in K \land F (P) \in A) \to \exists x \in J (P \in x \land F [x] \subseteq A)$

Metamath Proof Explorer