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		simpr	$⊢ (φ \land p \in (X \times X)) \to p \in (X \times X)$
24		elxp2	$⊢ p \in (X \times X) \leftrightarrow \exists x \in X \exists y \in X p = ⟨x, y⟩$
25	23 24	sylib	$⊢ (φ \land p \in (X \times X)) \to \exists x \in X \exists y \in X p = ⟨x, y⟩$
26		simpr	$⊢ (φ \land p = ⟨x, y⟩) \to p = ⟨x, y⟩$
27	26	eleq1d	$⊢ (φ \land p = ⟨x, y⟩) \to (p \in r \leftrightarrow ⟨x, y⟩ \in r)$
28	27	adantlr	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (p \in r \leftrightarrow ⟨x, y⟩ \in r)$
29		df-br	$⊢ x r y \leftrightarrow ⟨x, y⟩ \in r$
30	28 29	bitr4di	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (p \in r \leftrightarrow x r y)$
31		simplr	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to p \in (X \times X)$
32		opex	$⊢ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩ \in V$
33	1 2 3 4 5	ucnimalem	$⊢ G = (p \in (X \times X) ⟼ ⟨F (1^{st} (p)), F (2^{nd} (p))⟩)$
34	33	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))⟩$
35	31 32 34	sylancl	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to G (p) = ⟨F (1^{st} (p)), F (2^{nd} (p))⟩$
36		simpr	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to p = ⟨x, y⟩$
37		1st2nd2	$⊢ p \in (X \times X) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
38	31 37	syl	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
39	36 38	eqtr3d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to ⟨x, y⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩$
40		vex	$⊢ x \in V$
41		vex	$⊢ y \in V$
42	40 41	opth	$⊢ ⟨x, y⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩ \leftrightarrow (x = 1^{st} (p) \land y = 2^{nd} (p))$
43	39 42	sylib	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (x = 1^{st} (p) \land y = 2^{nd} (p))$
44	43	simpld	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to x = 1^{st} (p)$
45	44	fveq2d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to F (x) = F (1^{st} (p))$
46	43	simprd	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to y = 2^{nd} (p)$
47	46	fveq2d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to F (y) = F (2^{nd} (p))$
48	45 47	opeq12d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to ⟨F (x), F (y)⟩ = ⟨F (1^{st} (p)), F (2^{nd} (p))⟩$
49	35 48	eqtr4d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to G (p) = ⟨F (x), F (y)⟩$
50	49	eleq1d	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (G (p) \in W \leftrightarrow ⟨F (x), F (y)⟩ \in W)$
51		df-br	$⊢ F (x) W F (y) \leftrightarrow ⟨F (x), F (y)⟩ \in W$
52	50 51	bitr4di	$⊢ ((φ \land p \in (X \times X)) \land p = ⟨x, y⟩) \to (G (p) \in W \leftrightarrow F (x) W F (y))$
53	30 52	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)))$
54	53	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)))$
55	54	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)))$
56	55	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)))$
57	25 56	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))$
58	57	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))$
59	22 58	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)))$
60		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)$
61	60	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)$
62	61	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)$
63	59 62	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)$
64	63	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$
65	15 16 20 21 64	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$
66	65	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$
67	66	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)$
68	67	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)$
69	14 68	mpd	$⊢ φ \to \exists r \in U \forall p \in r G (p) \in W$
70	5	mpofun	$⊢ Fun G$
71		opex	$⊢ ⟨F (x), F (y)⟩ \in V$
72	5 71	dmmpo	$⊢ dom G = X \times X$
73	18 72	sseqtrrdi	$⊢ (φ \land r \in U) \to r \subseteq dom G$
74		funimass4	$⊢ (Fun G \land r \subseteq dom G) \to (G [r] \subseteq W \leftrightarrow \forall p \in r G (p) \in W)$
75	70 73 74	sylancr	$⊢ (φ \land r \in U) \to (G [r] \subseteq W \leftrightarrow \forall p \in r G (p) \in W)$
76	75	biimprd	$⊢ (φ \land r \in U) \to (\forall p \in r G (p) \in W \to G [r] \subseteq W)$
77	76	ralrimiva	$⊢ φ \to \forall r \in U (\forall p \in r G (p) \in W \to G [r] \subseteq W)$
78		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))$
79	69 77 78	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))$
80		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$
81	80	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$
82	79 81	syl	$⊢ φ \to \exists r \in U G [r] \subseteq W$

Metamath Proof Explorer

Theorem ucnima

Proof