metcnp3

Description: Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of Gleason p. 240. (Contributed by NM, 17-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	metcn.2	$⊢ J = MetOpen (C)$
	metcn.4	$⊢ K = MetOpen (D)$
Assertion	metcnp3	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y))$

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3	1	mopntopon	$⊢ C \in ∞Met (X) \to J \in TopOn (X)$
4	3	3ad2ant1	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to J \in TopOn (X)$
5	2	mopnval	$⊢ D \in ∞Met (Y) \to K = topGen (ran ball (D))$
6	5	3ad2ant2	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to K = topGen (ran ball (D))$
7	2	mopntopon	$⊢ D \in ∞Met (Y) \to K \in TopOn (Y)$
8	7	3ad2ant2	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to K \in TopOn (Y)$
9		simp3	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to P \in X$
10	4 6 8 9	tgcnp	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))))$
11		simpll2	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to D \in ∞Met (Y)$
12		simplr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to F : X ⟶ Y$
13		simpll3	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to P \in X$
14	12 13	ffvelrnd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to F (P) \in Y$
15		simpr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
16		blcntr	$⊢ (D \in ∞Met (Y) \land F (P) \in Y \land y \in ℝ^{+}) \to F (P) \in (F (P) ball (D) y)$
17	11 14 15 16	syl3anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to F (P) \in (F (P) ball (D) y)$
18		rpxr	$⊢ y \in ℝ^{+} \to y \in ℝ^{*}$
19	18	adantl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to y \in ℝ^{*}$
20		blelrn	$⊢ (D \in ∞Met (Y) \land F (P) \in Y \land y \in ℝ^{*}) \to F (P) ball (D) y \in ran ball (D)$
21	11 14 19 20	syl3anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to F (P) ball (D) y \in ran ball (D)$
22		eleq2	$⊢ u = F (P) ball (D) y \to (F (P) \in u \leftrightarrow F (P) \in (F (P) ball (D) y))$
23		sseq2	$⊢ u = F (P) ball (D) y \to (F [v] \subseteq u \leftrightarrow F [v] \subseteq F (P) ball (D) y)$
24	23	anbi2d	$⊢ u = F (P) ball (D) y \to ((P \in v \land F [v] \subseteq u) \leftrightarrow (P \in v \land F [v] \subseteq F (P) ball (D) y))$
25	24	rexbidv	$⊢ u = F (P) ball (D) y \to (\exists v \in J (P \in v \land F [v] \subseteq u) \leftrightarrow \exists v \in J (P \in v \land F [v] \subseteq F (P) ball (D) y))$
26	22 25	imbi12d	$⊢ u = F (P) ball (D) y \to ((F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \leftrightarrow (F (P) \in (F (P) ball (D) y) \to \exists v \in J (P \in v \land F [v] \subseteq F (P) ball (D) y)))$
27	26	rspcv	$⊢ F (P) ball (D) y \in ran ball (D) \to (\forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \to (F (P) \in (F (P) ball (D) y) \to \exists v \in J (P \in v \land F [v] \subseteq F (P) ball (D) y)))$
28	21 27	syl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to (\forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \to (F (P) \in (F (P) ball (D) y) \to \exists v \in J (P \in v \land F [v] \subseteq F (P) ball (D) y)))$
29	17 28	mpid	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to (\forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \to \exists v \in J (P \in v \land F [v] \subseteq F (P) ball (D) y))$
30		simpl1	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to C \in ∞Met (X)$
31	30	ad2antrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land v \in J)) \land P \in v) \to C \in ∞Met (X)$
32		simplrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land v \in J)) \land P \in v) \to v \in J$
33		simpr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land v \in J)) \land P \in v) \to P \in v$
34	1	mopni2	$⊢ (C \in ∞Met (X) \land v \in J \land P \in v) \to \exists z \in ℝ^{+} P ball (C) z \subseteq v$
35	31 32 33 34	syl3anc	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land v \in J)) \land P \in v) \to \exists z \in ℝ^{+} P ball (C) z \subseteq v$
36		sstr2	$⊢ F [P ball (C) z] \subseteq F [v] \to (F [v] \subseteq F (P) ball (D) y \to F [P ball (C) z] \subseteq F (P) ball (D) y)$
37		imass2	$⊢ P ball (C) z \subseteq v \to F [P ball (C) z] \subseteq F [v]$
38	36 37	syl11	$⊢ F [v] \subseteq F (P) ball (D) y \to (P ball (C) z \subseteq v \to F [P ball (C) z] \subseteq F (P) ball (D) y)$
39	38	reximdv	$⊢ F [v] \subseteq F (P) ball (D) y \to (\exists z \in ℝ^{+} P ball (C) z \subseteq v \to \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
40	35 39	syl5com	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land v \in J)) \land P \in v) \to (F [v] \subseteq F (P) ball (D) y \to \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
41	40	expimpd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land v \in J)) \to ((P \in v \land F [v] \subseteq F (P) ball (D) y) \to \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
42	41	expr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to (v \in J \to ((P \in v \land F [v] \subseteq F (P) ball (D) y) \to \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y))$
43	42	rexlimdv	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to (\exists v \in J (P \in v \land F [v] \subseteq F (P) ball (D) y) \to \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
44	29 43	syld	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to (\forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \to \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
45	44	ralrimdva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \to \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
46		simpl2	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to D \in ∞Met (Y)$
47		blss	$⊢ (D \in ∞Met (Y) \land u \in ran ball (D) \land F (P) \in u) \to \exists y \in ℝ^{+} F (P) ball (D) y \subseteq u$
48	47	3expib	$⊢ D \in ∞Met (Y) \to ((u \in ran ball (D) \land F (P) \in u) \to \exists y \in ℝ^{+} F (P) ball (D) y \subseteq u)$
49	46 48	syl	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to ((u \in ran ball (D) \land F (P) \in u) \to \exists y \in ℝ^{+} F (P) ball (D) y \subseteq u)$
50		r19.29r	$⊢ (\exists y \in ℝ^{+} F (P) ball (D) y \subseteq u \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y) \to \exists y \in ℝ^{+} (F (P) ball (D) y \subseteq u \land \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
51	30	ad5ant12	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to C \in ∞Met (X)$
52	13	ad2antrr	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to P \in X$
53		rpxr	$⊢ z \in ℝ^{+} \to z \in ℝ^{*}$
54	53	ad2antrl	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to z \in ℝ^{*}$
55	1	blopn	$⊢ (C \in ∞Met (X) \land P \in X \land z \in ℝ^{*}) \to P ball (C) z \in J$
56	51 52 54 55	syl3anc	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to P ball (C) z \in J$
57		simprl	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to z \in ℝ^{+}$
58		blcntr	$⊢ (C \in ∞Met (X) \land P \in X \land z \in ℝ^{+}) \to P \in (P ball (C) z)$
59	51 52 57 58	syl3anc	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to P \in (P ball (C) z)$
60		sstr	$⊢ (F [P ball (C) z] \subseteq F (P) ball (D) y \land F (P) ball (D) y \subseteq u) \to F [P ball (C) z] \subseteq u$
61	60	ad2ant2l	$⊢ ((z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y) \land ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u)) \to F [P ball (C) z] \subseteq u$
62	61	ancoms	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to F [P ball (C) z] \subseteq u$
63		eleq2	$⊢ v = P ball (C) z \to (P \in v \leftrightarrow P \in (P ball (C) z))$
64		imaeq2	$⊢ v = P ball (C) z \to F [v] = F [P ball (C) z]$
65	64	sseq1d	$⊢ v = P ball (C) z \to (F [v] \subseteq u \leftrightarrow F [P ball (C) z] \subseteq u)$
66	63 65	anbi12d	$⊢ v = P ball (C) z \to ((P \in v \land F [v] \subseteq u) \leftrightarrow (P \in (P ball (C) z) \land F [P ball (C) z] \subseteq u))$
67	66	rspcev	$⊢ (P ball (C) z \in J \land (P \in (P ball (C) z) \land F [P ball (C) z] \subseteq u)) \to \exists v \in J (P \in v \land F [v] \subseteq u)$
68	56 59 62 67	syl12anc	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land (z \in ℝ^{+} \land F [P ball (C) z] \subseteq F (P) ball (D) y)) \to \exists v \in J (P \in v \land F [v] \subseteq u)$
69	68	expr	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \land z \in ℝ^{+}) \to (F [P ball (C) z] \subseteq F (P) ball (D) y \to \exists v \in J (P \in v \land F [v] \subseteq u))$
70	69	rexlimdva	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land F (P) ball (D) y \subseteq u) \to (\exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \to \exists v \in J (P \in v \land F [v] \subseteq u))$
71	70	expimpd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to ((F (P) ball (D) y \subseteq u \land \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y) \to \exists v \in J (P \in v \land F [v] \subseteq u))$
72	71	rexlimdva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\exists y \in ℝ^{+} (F (P) ball (D) y \subseteq u \land \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y) \to \exists v \in J (P \in v \land F [v] \subseteq u))$
73	50 72	syl5	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to ((\exists y \in ℝ^{+} F (P) ball (D) y \subseteq u \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y) \to \exists v \in J (P \in v \land F [v] \subseteq u))$
74	73	expd	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\exists y \in ℝ^{+} F (P) ball (D) y \subseteq u \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \to \exists v \in J (P \in v \land F [v] \subseteq u)))$
75	49 74	syld	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to ((u \in ran ball (D) \land F (P) \in u) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \to \exists v \in J (P \in v \land F [v] \subseteq u)))$
76	75	com23	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \to ((u \in ran ball (D) \land F (P) \in u) \to \exists v \in J (P \in v \land F [v] \subseteq u)))$
77	76	exp4a	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \to (u \in ran ball (D) \to (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))))$
78	77	ralrimdv	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \to \forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)))$
79	45 78	impbid	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u)) \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y)$
80	79	pm5.32da	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to ((F : X ⟶ Y \land \forall u \in ran ball (D) (F (P) \in u \to \exists v \in J (P \in v \land F [v] \subseteq u))) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y))$
81	10 80	bitrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y))$

Metamath Proof Explorer

Theorem metcnp3

Proof