ucnima

Description: An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017)

	Ref	Expression
Hypotheses	ucnprima.1	$⊢ φ \to U \in UnifOn (X)$
	ucnprima.2	$⊢ φ \to V \in UnifOn (Y)$
	ucnprima.3	$⊢ φ \to F \in (U uCn V)$
	ucnprima.4	$⊢ φ \to W \in V$
	ucnprima.5	$⊢ G = (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)$
Assertion	ucnima	$⊢ φ \to \exists r \in U G [r] \subseteq W$

Proof

Step	Hyp	Ref	Expression
1		ucnprima.1	$⊢ φ \to U \in UnifOn (X)$
2		ucnprima.2	$⊢ φ \to V \in UnifOn (Y)$
3		ucnprima.3	$⊢ φ \to F \in (U uCn V)$
4		ucnprima.4	$⊢ φ \to W \in V$
5		ucnprima.5	$⊢ G = (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)$
6		breq	$⊢ w = W \to (F (x) w F (y) \leftrightarrow F (x) W F (y))$
7	6	imbi2d	$⊢ w = W \to ((x r y \to F (x) w F (y)) \leftrightarrow (x r y \to F (x) W F (y)))$
8	7	ralbidv	$⊢ w = W \to (\forall y \in X (x r y \to F (x) w F (y)) \leftrightarrow \forall y \in X (x r y \to F (x) W F (y)))$
9	8	rexralbidv	$⊢ w = W \to (\exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) w F (y)) \leftrightarrow \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) W F (y)))$
10		isucn	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall w \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) w F (y))))$
11	1 2 10	syl2anc	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall w \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) w F (y))))$
12	3 11	mpbid	$⊢ φ \to (F : X ⟶ Y \land \forall w \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) w F (y)))$
13	12	simprd	$⊢ φ \to \forall w \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) w F (y))$
14	9 13 4	rspcdva	$⊢ φ \to \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) W F (y))$
15		simplll	$⊢ (((φ \land r \in U) \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in r) \to φ$
16		simplr	$⊢ (((φ \land r \in U) \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in r) \to \forall x \in X \forall y \in X (x r y \to F (x) W F (y))$
17		ustssxp	$⊢ (U \in UnifOn (X) \land r \in U) \to r \subseteq X \times X$
18	1 17	sylan	$⊢ (φ \land r \in U) \to r \subseteq X \times X$
19	18	sselda	$⊢ ((φ \land r \in U) \land p \in r) \to p \in (X \times X)$
20	19	adantlr	$⊢ (((φ \land r \in U) \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in r) \to p \in (X \times X)$
21		simpr	$⊢ (((φ \land r \in U) \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in r) \to p \in r$
22		simplr	$⊢ ((φ \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in (X \times X)) \to \forall x \in X \forall y \in X (x r y \to F (x) W F (y))$
23		elxp2	$⊢ p \in (X \times X) \leftrightarrow \exists x \in X \exists y \in X p = ⟨x, y⟩$
24	23	bilani	$⊢ (φ \land p \in (X \times X)) \to \exists x \in X \exists y \in X p = ⟨x, y⟩$
25		simpr	$⊢ (φ \land p = ⟨x, y⟩) \to p = ⟨x, y⟩$
26	25	eleq1d	$⊢ (φ \land p = ⟨x, y⟩) \to (p \in r \leftrightarrow ⟨x, y⟩ \in r)$
27	26	adantlr	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (p \in r \leftrightarrow ⟨x, y⟩ \in r)$
28		df-br	$⊢ x r y \leftrightarrow ⟨x, y⟩ \in r$
29	27 28	bitr4di	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (p \in r \leftrightarrow x r y)$
30		simplr	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to p \in (X \times X)$
31		opex	$⊢ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩ \in V$
32	1 2 3 4 5	ucnimalem	$⊢ G = (p \in (X \times X) ⟼ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩)$
33	32	fvmpt2	$⊢ (p \in (X \times X) \land ⟨F (1^{st} (p)), F (2^{nd} (p))⟩ \in V) \to G (p) = ⟨F (1^{st} (p)), F (2^{nd} (p))⟩$
34	30 31 33	sylancl	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to G (p) = ⟨F (1^{st} (p)), F (2^{nd} (p))⟩$
35		simpr	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to p = ⟨x, y⟩$
36		1st2nd2	$⊢ p \in (X \times X) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
37	30 36	syl	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
38	35 37	eqtr3d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to ⟨x, y⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩$
39		vex	$⊢ x \in V$
40		vex	$⊢ y \in V$
41	39 40	opth	$⊢ ⟨x, y⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩ \leftrightarrow (x = 1^{st} (p) \land y = 2^{nd} (p))$
42	38 41	sylib	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (x = 1^{st} (p) \land y = 2^{nd} (p))$
43	42	simpld	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to x = 1^{st} (p)$
44	43	fveq2d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to F (x) = F (1^{st} (p))$
45	42	simprd	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to y = 2^{nd} (p)$
46	45	fveq2d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to F (y) = F (2^{nd} (p))$
47	44 46	opeq12d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to ⟨F (x), F (y)⟩ = ⟨F (1^{st} (p)), F (2^{nd} (p))⟩$
48	34 47	eqtr4d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to G (p) = ⟨F (x), F (y)⟩$
49	48	eleq1d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (G (p) \in W \leftrightarrow ⟨F (x), F (y)⟩ \in W)$
50		df-br	$⊢ F (x) W F (y) \leftrightarrow ⟨F (x), F (y)⟩ \in W$
51	49 50	bitr4di	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (G (p) \in W \leftrightarrow F (x) W F (y))$
52	29 51	imbi12d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to ((p \in r \to G (p) \in W) \leftrightarrow (x r y \to F (x) W F (y)))$
53	52	exbiri	$⊢ (φ \land p \in (X \times X)) \to (p = ⟨x, y⟩ \to ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W)))$
54	53	reximdv	$⊢ (φ \land p \in (X \times X)) \to (\exists y \in X p = ⟨x, y⟩ \to \exists y \in X ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W)))$
55	54	reximdv	$⊢ (φ \land p \in (X \times X)) \to (\exists x \in X \exists y \in X p = ⟨x, y⟩ \to \exists x \in X \exists y \in X ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W)))$
56	24 55	mpd	$⊢ (φ \land p \in (X \times X)) \to \exists x \in X \exists y \in X ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W))$
57	56	adantlr	$⊢ ((φ \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in (X \times X)) \to \exists x \in X \exists y \in X ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W))$
58	22 57	r19.29d2r	$⊢ ((φ \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in (X \times X)) \to \exists x \in X \exists y \in X ((x r y \to F (x) W F (y)) \land ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W)))$
59		pm3.35	$⊢ ((x r y \to F (x) W F (y)) \land ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W))) \to (p \in r \to G (p) \in W)$
60	59	rexlimivw	$⊢ \exists y \in X ((x r y \to F (x) W F (y)) \land ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W))) \to (p \in r \to G (p) \in W)$
61	60	rexlimivw	$⊢ \exists x \in X \exists y \in X ((x r y \to F (x) W F (y)) \land ((x r y \to F (x) W F (y)) \to (p \in r \to G (p) \in W))) \to (p \in r \to G (p) \in W)$
62	58 61	syl	$⊢ ((φ \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in (X \times X)) \to (p \in r \to G (p) \in W)$
63	62	imp	$⊢ (((φ \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in (X \times X)) \land p \in r) \to G (p) \in W$
64	15 16 20 21 63	syl1111anc	$⊢ (((φ \land r \in U) \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \land p \in r) \to G (p) \in W$
65	64	ralrimiva	$⊢ ((φ \land r \in U) \land \forall x \in X \forall y \in X (x r y \to F (x) W F (y))) \to \forall p \in r G (p) \in W$
66	65	ex	$⊢ (φ \land r \in U) \to (\forall x \in X \forall y \in X (x r y \to F (x) W F (y)) \to \forall p \in r G (p) \in W)$
67	66	reximdva	$⊢ φ \to (\exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) W F (y)) \to \exists r \in U \forall p \in r G (p) \in W)$
68	14 67	mpd	$⊢ φ \to \exists r \in U \forall p \in r G (p) \in W$
69	5	mpofun	$⊢ Fun G$
70		opex	$⊢ ⟨F (x), F (y)⟩ \in V$
71	5 70	dmmpo	$⊢ dom G = X \times X$
72	18 71	sseqtrrdi	$⊢ (φ \land r \in U) \to r \subseteq dom G$
73		funimass4	$⊢ (Fun G \land r \subseteq dom G) \to (G [r] \subseteq W \leftrightarrow \forall p \in r G (p) \in W)$
74	69 72 73	sylancr	$⊢ (φ \land r \in U) \to (G [r] \subseteq W \leftrightarrow \forall p \in r G (p) \in W)$
75	74	biimprd	$⊢ (φ \land r \in U) \to (\forall p \in r G (p) \in W \to G [r] \subseteq W)$
76	75	ralrimiva	$⊢ φ \to \forall r \in U (\forall p \in r G (p) \in W \to G [r] \subseteq W)$
77		r19.29r	$⊢ (\exists r \in U \forall p \in r G (p) \in W \land \forall r \in U (\forall p \in r G (p) \in W \to G [r] \subseteq W)) \to \exists r \in U (\forall p \in r G (p) \in W \land (\forall p \in r G (p) \in W \to G [r] \subseteq W))$
78	68 76 77	syl2anc	$⊢ φ \to \exists r \in U (\forall p \in r G (p) \in W \land (\forall p \in r G (p) \in W \to G [r] \subseteq W))$
79		pm3.35	$⊢ (\forall p \in r G (p) \in W \land (\forall p \in r G (p) \in W \to G [r] \subseteq W)) \to G [r] \subseteq W$
80	79	reximi	$⊢ \exists r \in U (\forall p \in r G (p) \in W \land (\forall p \in r G (p) \in W \to G [r] \subseteq W)) \to \exists r \in U G [r] \subseteq W$
81	78 80	syl	$⊢ φ \to \exists r \in U G [r] \subseteq W$

Metamath Proof Explorer

Theorem ucnima

Proof