metucn

Description: Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn . (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Hypotheses	metucn.u	$⊢ U = metUnif (C)$
	metucn.v	$⊢ V = metUnif (D)$
	metucn.x	$⊢ φ \to X \neq \emptyset$
	metucn.y	$⊢ φ \to Y \neq \emptyset$
	metucn.c	$⊢ φ \to C \in PsMet (X)$
	metucn.d	$⊢ φ \to D \in PsMet (Y)$
Assertion	metucn	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d)))$

Proof

Step	Hyp	Ref	Expression
1		metucn.u	$⊢ U = metUnif (C)$
2		metucn.v	$⊢ V = metUnif (D)$
3		metucn.x	$⊢ φ \to X \neq \emptyset$
4		metucn.y	$⊢ φ \to Y \neq \emptyset$
5		metucn.c	$⊢ φ \to C \in PsMet (X)$
6		metucn.d	$⊢ φ \to D \in PsMet (Y)$
7		metuval	$⊢ C \in PsMet (X) \to metUnif (C) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])$
8	5 7	syl	$⊢ φ \to metUnif (C) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])$
9	1 8	syl5eq	$⊢ φ \to U = (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])$
10		metuval	$⊢ D \in PsMet (Y) \to metUnif (D) = (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
11	6 10	syl	$⊢ φ \to metUnif (D) = (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
12	2 11	syl5eq	$⊢ φ \to V = (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
13	9 12	oveq12d	$⊢ φ \to U uCn V = ((X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])) uCn ((Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]))$
14	13	eleq2d	$⊢ φ \to (F \in (U uCn V) \leftrightarrow F \in (((X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])) uCn ((Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]))))$
15		eqid	$⊢ (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])$
16		eqid	$⊢ (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) = (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
17		oveq2	$⊢ a = c \to [0, a) = [0, c)$
18	17	imaeq2d	$⊢ a = c \to C^{-1} [[0, a)] = C^{-1} [[0, c)]$
19	18	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) = (c \in ℝ^{+} ⟼ C^{-1} [[0, c)])$
20	19	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) = ran (c \in ℝ^{+} ⟼ C^{-1} [[0, c)])$
21	20	metust	$⊢ (X \neq \emptyset \land C \in PsMet (X)) \to (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \in UnifOn (X)$
22	3 5 21	syl2anc	$⊢ φ \to (X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \in UnifOn (X)$
23		oveq2	$⊢ b = d \to [0, b) = [0, d)$
24	23	imaeq2d	$⊢ b = d \to D^{-1} [[0, b)] = D^{-1} [[0, d)]$
25	24	cbvmptv	$⊢ (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) = (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
26	25	rneqi	$⊢ ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) = ran (d \in ℝ^{+} ⟼ D^{-1} [[0, d)])$
27	26	metust	$⊢ (Y \neq \emptyset \land D \in PsMet (Y)) \to (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \in UnifOn (Y)$
28	4 6 27	syl2anc	$⊢ φ \to (Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \in UnifOn (Y)$
29		oveq2	$⊢ a = e \to [0, a) = [0, e)$
30	29	imaeq2d	$⊢ a = e \to C^{-1} [[0, a)] = C^{-1} [[0, e)]$
31	30	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) = (e \in ℝ^{+} ⟼ C^{-1} [[0, e)])$
32	31	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) = ran (e \in ℝ^{+} ⟼ C^{-1} [[0, e)])$
33	32	metustfbas	$⊢ (X \neq \emptyset \land C \in PsMet (X)) \to ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \in fBas (X \times X)$
34	3 5 33	syl2anc	$⊢ φ \to ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \in fBas (X \times X)$
35		oveq2	$⊢ b = f \to [0, b) = [0, f)$
36	35	imaeq2d	$⊢ b = f \to D^{-1} [[0, b)] = D^{-1} [[0, f)]$
37	36	cbvmptv	$⊢ (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) = (f \in ℝ^{+} ⟼ D^{-1} [[0, f)])$
38	37	rneqi	$⊢ ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) = ran (f \in ℝ^{+} ⟼ D^{-1} [[0, f)])$
39	38	metustfbas	$⊢ (Y \neq \emptyset \land D \in PsMet (Y)) \to ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \in fBas (Y \times Y)$
40	4 6 39	syl2anc	$⊢ φ \to ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \in fBas (Y \times Y)$
41	15 16 22 28 34 40	isucn2	$⊢ φ \to (F \in (((X \times X) filGen ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])) uCn ((Y \times Y) filGen ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]))) \leftrightarrow (F : X ⟶ Y \land \forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y))))$
42	14 41	bitrd	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y))))$
43		eqid	$⊢ D^{-1} [[0, d)] = D^{-1} [[0, d)]$
44		oveq2	$⊢ f = d \to [0, f) = [0, d)$
45	44	imaeq2d	$⊢ f = d \to D^{-1} [[0, f)] = D^{-1} [[0, d)]$
46	45	rspceeqv	$⊢ (d \in ℝ^{+} \land D^{-1} [[0, d)] = D^{-1} [[0, d)]) \to \exists f \in ℝ^{+} D^{-1} [[0, d)] = D^{-1} [[0, f)]$
47	43 46	mpan2	$⊢ d \in ℝ^{+} \to \exists f \in ℝ^{+} D^{-1} [[0, d)] = D^{-1} [[0, f)]$
48	47	adantl	$⊢ (φ \land d \in ℝ^{+}) \to \exists f \in ℝ^{+} D^{-1} [[0, d)] = D^{-1} [[0, f)]$
49	38	metustel	$⊢ D \in PsMet (Y) \to (D^{-1} [[0, d)] \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \leftrightarrow \exists f \in ℝ^{+} D^{-1} [[0, d)] = D^{-1} [[0, f)])$
50	6 49	syl	$⊢ φ \to (D^{-1} [[0, d)] \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \leftrightarrow \exists f \in ℝ^{+} D^{-1} [[0, d)] = D^{-1} [[0, f)])$
51	50	adantr	$⊢ (φ \land d \in ℝ^{+}) \to (D^{-1} [[0, d)] \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \leftrightarrow \exists f \in ℝ^{+} D^{-1} [[0, d)] = D^{-1} [[0, f)])$
52	48 51	mpbird	$⊢ (φ \land d \in ℝ^{+}) \to D^{-1} [[0, d)] \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
53	26	metustel	$⊢ D \in PsMet (Y) \to (v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \leftrightarrow \exists d \in ℝ^{+} v = D^{-1} [[0, d)])$
54	6 53	syl	$⊢ φ \to (v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \leftrightarrow \exists d \in ℝ^{+} v = D^{-1} [[0, d)])$
55		simpr	$⊢ (φ \land v = D^{-1} [[0, d)]) \to v = D^{-1} [[0, d)]$
56	55	breqd	$⊢ (φ \land v = D^{-1} [[0, d)]) \to (F (x) v F (y) \leftrightarrow F (x) D^{-1} [[0, d)] F (y))$
57	56	imbi2d	$⊢ (φ \land v = D^{-1} [[0, d)]) \to ((x u y \to F (x) v F (y)) \leftrightarrow (x u y \to F (x) D^{-1} [[0, d)] F (y)))$
58	57	ralbidv	$⊢ (φ \land v = D^{-1} [[0, d)]) \to (\forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \forall y \in X (x u y \to F (x) D^{-1} [[0, d)] F (y)))$
59	58	rexralbidv	$⊢ (φ \land v = D^{-1} [[0, d)]) \to (\exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) D^{-1} [[0, d)] F (y)))$
60	52 54 59	ralxfr2d	$⊢ φ \to (\forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \forall d \in ℝ^{+} \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) D^{-1} [[0, d)] F (y)))$
61		eqid	$⊢ C^{-1} [[0, c)] = C^{-1} [[0, c)]$
62		oveq2	$⊢ e = c \to [0, e) = [0, c)$
63	62	imaeq2d	$⊢ e = c \to C^{-1} [[0, e)] = C^{-1} [[0, c)]$
64	63	rspceeqv	$⊢ (c \in ℝ^{+} \land C^{-1} [[0, c)] = C^{-1} [[0, c)]) \to \exists e \in ℝ^{+} C^{-1} [[0, c)] = C^{-1} [[0, e)]$
65	61 64	mpan2	$⊢ c \in ℝ^{+} \to \exists e \in ℝ^{+} C^{-1} [[0, c)] = C^{-1} [[0, e)]$
66	65	adantl	$⊢ (φ \land c \in ℝ^{+}) \to \exists e \in ℝ^{+} C^{-1} [[0, c)] = C^{-1} [[0, e)]$
67	32	metustel	$⊢ C \in PsMet (X) \to (C^{-1} [[0, c)] \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \leftrightarrow \exists e \in ℝ^{+} C^{-1} [[0, c)] = C^{-1} [[0, e)])$
68	5 67	syl	$⊢ φ \to (C^{-1} [[0, c)] \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \leftrightarrow \exists e \in ℝ^{+} C^{-1} [[0, c)] = C^{-1} [[0, e)])$
69	68	adantr	$⊢ (φ \land c \in ℝ^{+}) \to (C^{-1} [[0, c)] \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \leftrightarrow \exists e \in ℝ^{+} C^{-1} [[0, c)] = C^{-1} [[0, e)])$
70	66 69	mpbird	$⊢ (φ \land c \in ℝ^{+}) \to C^{-1} [[0, c)] \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)])$
71	20	metustel	$⊢ C \in PsMet (X) \to (u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \leftrightarrow \exists c \in ℝ^{+} u = C^{-1} [[0, c)])$
72	5 71	syl	$⊢ φ \to (u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \leftrightarrow \exists c \in ℝ^{+} u = C^{-1} [[0, c)])$
73		simpr	$⊢ (φ \land u = C^{-1} [[0, c)]) \to u = C^{-1} [[0, c)]$
74	73	breqd	$⊢ (φ \land u = C^{-1} [[0, c)]) \to (x u y \leftrightarrow x C^{-1} [[0, c)] y)$
75	74	imbi1d	$⊢ (φ \land u = C^{-1} [[0, c)]) \to ((x u y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)))$
76	75	2ralbidv	$⊢ (φ \land u = C^{-1} [[0, c)]) \to (\forall x \in X \forall y \in X (x u y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)))$
77	70 72 76	rexxfr2d	$⊢ φ \to (\exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)))$
78	77	ralbidv	$⊢ φ \to (\forall d \in ℝ^{+} \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)))$
79	60 78	bitrd	$⊢ φ \to (\forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)))$
80	79	adantr	$⊢ (φ \land F : X ⟶ Y) \to (\forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)))$
81	5	ad4antr	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to C \in PsMet (X)$
82		simplr	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to c \in ℝ^{+}$
83		simprr	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to y \in X$
84		simprl	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to x \in X$
85		elbl4	$⊢ ((C \in PsMet (X) \land c \in ℝ^{+}) \land (y \in X \land x \in X)) \to (x \in (y ball (C) c) \leftrightarrow x C^{-1} [[0, c)] y)$
86		rpxr	$⊢ c \in ℝ^{+} \to c \in ℝ^{*}$
87		elbl3ps	$⊢ ((C \in PsMet (X) \land c \in ℝ^{*}) \land (y \in X \land x \in X)) \to (x \in (y ball (C) c) \leftrightarrow x C y < c)$
88	86 87	sylanl2	$⊢ ((C \in PsMet (X) \land c \in ℝ^{+}) \land (y \in X \land x \in X)) \to (x \in (y ball (C) c) \leftrightarrow x C y < c)$
89	85 88	bitr3d	$⊢ ((C \in PsMet (X) \land c \in ℝ^{+}) \land (y \in X \land x \in X)) \to (x C^{-1} [[0, c)] y \leftrightarrow x C y < c)$
90	81 82 83 84 89	syl22anc	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to (x C^{-1} [[0, c)] y \leftrightarrow x C y < c)$
91	6	ad4antr	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to D \in PsMet (Y)$
92		simpllr	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to d \in ℝ^{+}$
93		simp-4r	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to F : X ⟶ Y$
94	93 83	ffvelrnd	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to F (y) \in Y$
95	93 84	ffvelrnd	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to F (x) \in Y$
96		elbl4	$⊢ ((D \in PsMet (Y) \land d \in ℝ^{+}) \land (F (y) \in Y \land F (x) \in Y)) \to (F (x) \in (F (y) ball (D) d) \leftrightarrow F (x) D^{-1} [[0, d)] F (y))$
97		rpxr	$⊢ d \in ℝ^{+} \to d \in ℝ^{*}$
98		elbl3ps	$⊢ ((D \in PsMet (Y) \land d \in ℝ^{*}) \land (F (y) \in Y \land F (x) \in Y)) \to (F (x) \in (F (y) ball (D) d) \leftrightarrow F (x) D F (y) < d)$
99	97 98	sylanl2	$⊢ ((D \in PsMet (Y) \land d \in ℝ^{+}) \land (F (y) \in Y \land F (x) \in Y)) \to (F (x) \in (F (y) ball (D) d) \leftrightarrow F (x) D F (y) < d)$
100	96 99	bitr3d	$⊢ ((D \in PsMet (Y) \land d \in ℝ^{+}) \land (F (y) \in Y \land F (x) \in Y)) \to (F (x) D^{-1} [[0, d)] F (y) \leftrightarrow F (x) D F (y) < d)$
101	91 92 94 95 100	syl22anc	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to (F (x) D^{-1} [[0, d)] F (y) \leftrightarrow F (x) D F (y) < d)$
102	90 101	imbi12d	$⊢ ((((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \land (x \in X \land y \in X)) \to ((x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow (x C y < c \to F (x) D F (y) < d))$
103	102	2ralbidva	$⊢ (((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \land c \in ℝ^{+}) \to (\forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d))$
104	103	rexbidva	$⊢ ((φ \land F : X ⟶ Y) \land d \in ℝ^{+}) \to (\exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d))$
105	104	ralbidva	$⊢ (φ \land F : X ⟶ Y) \to (\forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C^{-1} [[0, c)] y \to F (x) D^{-1} [[0, d)] F (y)) \leftrightarrow \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d))$
106	80 105	bitrd	$⊢ (φ \land F : X ⟶ Y) \to (\forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d))$
107	106	pm5.32da	$⊢ φ \to ((F : X ⟶ Y \land \forall v \in ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)]) \exists u \in ran (a \in ℝ^{+} ⟼ C^{-1} [[0, a)]) \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \leftrightarrow (F : X ⟶ Y \land \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d)))$
108	42 107	bitrd	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall d \in ℝ^{+} \exists c \in ℝ^{+} \forall x \in X \forall y \in X (x C y < c \to F (x) D F (y) < d)))$

Metamath Proof Explorer

Theorem metucn

Proof