isucn2

Description: The predicate " F is a uniformly continuous function from uniform space U to uniform space V ", expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018)

	Ref	Expression
Hypotheses	isucn2.u	$⊢ U = (X \times X) filGen R$
	isucn2.v	$⊢ V = (Y \times Y) filGen S$
	isucn2.1	$⊢ φ \to U \in UnifOn (X)$
	isucn2.2	$⊢ φ \to V \in UnifOn (Y)$
	isucn2.3	$⊢ φ \to R \in fBas (X \times X)$
	isucn2.4	$⊢ φ \to S \in fBas (Y \times Y)$
Assertion	isucn2	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y))))$

Proof

Step	Hyp	Ref	Expression
1		isucn2.u	$⊢ U = (X \times X) filGen R$
2		isucn2.v	$⊢ V = (Y \times Y) filGen S$
3		isucn2.1	$⊢ φ \to U \in UnifOn (X)$
4		isucn2.2	$⊢ φ \to V \in UnifOn (Y)$
5		isucn2.3	$⊢ φ \to R \in fBas (X \times X)$
6		isucn2.4	$⊢ φ \to S \in fBas (Y \times Y)$
7		isucn	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))))$
8	3 4 7	syl2anc	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))))$
9		breq	$⊢ v = s \to (F (x) v F (y) \leftrightarrow F (x) s F (y))$
10	9	imbi2d	$⊢ v = s \to ((x u y \to F (x) v F (y)) \leftrightarrow (x u y \to F (x) s F (y)))$
11	10	ralbidv	$⊢ v = s \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) s F (y)))$
12	11	rexralbidv	$⊢ v = s \to (\exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
13		simplr	$⊢ (((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \land s \in S) \to \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))$
14		ssfg	$⊢ S \in fBas (Y \times Y) \to S \subseteq (Y \times Y) filGen S$
15	6 14	syl	$⊢ φ \to S \subseteq (Y \times Y) filGen S$
16	15 2	sseqtrrdi	$⊢ φ \to S \subseteq V$
17	16	adantr	$⊢ (φ \land F : X ⟶ Y) \to S \subseteq V$
18	17	adantr	$⊢ ((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \to S \subseteq V$
19	18	sselda	$⊢ (((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \land s \in S) \to s \in V$
20	12 13 19	rspcdva	$⊢ (((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \land s \in S) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))$
21		simpr	$⊢ (φ \land u \in U) \to u \in U$
22	21 1	eleqtrdi	$⊢ (φ \land u \in U) \to u \in ((X \times X) filGen R)$
23		elfg	$⊢ R \in fBas (X \times X) \to (u \in ((X \times X) filGen R) \leftrightarrow (u \subseteq X \times X \land \exists r \in R r \subseteq u))$
24	5 23	syl	$⊢ φ \to (u \in ((X \times X) filGen R) \leftrightarrow (u \subseteq X \times X \land \exists r \in R r \subseteq u))$
25	24	simplbda	$⊢ (φ \land u \in ((X \times X) filGen R)) \to \exists r \in R r \subseteq u$
26	22 25	syldan	$⊢ (φ \land u \in U) \to \exists r \in R r \subseteq u$
27		ssbr	$⊢ r \subseteq u \to (x r y \to x u y)$
28	27	imim1d	$⊢ r \subseteq u \to ((x u y \to F (x) s F (y)) \to (x r y \to F (x) s F (y)))$
29	28	adantl	$⊢ ((φ \land r \in R) \land r \subseteq u) \to ((x u y \to F (x) s F (y)) \to (x r y \to F (x) s F (y)))$
30	29	ralrimivw	$⊢ ((φ \land r \in R) \land r \subseteq u) \to \forall y \in X ((x u y \to F (x) s F (y)) \to (x r y \to F (x) s F (y)))$
31	30	ralrimivw	$⊢ ((φ \land r \in R) \land r \subseteq u) \to \forall x \in X \forall y \in X ((x u y \to F (x) s F (y)) \to (x r y \to F (x) s F (y)))$
32		ralim	$⊢ \forall y \in X ((x u y \to F (x) s F (y)) \to (x r y \to F (x) s F (y))) \to (\forall y \in X (x u y \to F (x) s F (y)) \to \forall y \in X (x r y \to F (x) s F (y)))$
33	32	ralimi	$⊢ \forall x \in X \forall y \in X ((x u y \to F (x) s F (y)) \to (x r y \to F (x) s F (y))) \to \forall x \in X (\forall y \in X (x u y \to F (x) s F (y)) \to \forall y \in X (x r y \to F (x) s F (y)))$
34		ralim	$⊢ \forall x \in X (\forall y \in X (x u y \to F (x) s F (y)) \to \forall y \in X (x r y \to F (x) s F (y))) \to (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
35	31 33 34	3syl	$⊢ ((φ \land r \in R) \land r \subseteq u) \to (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
36	35	ex	$⊢ (φ \land r \in R) \to (r \subseteq u \to (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y))))$
37	36	reximdva	$⊢ φ \to (\exists r \in R r \subseteq u \to \exists r \in R (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y))))$
38	37	adantr	$⊢ (φ \land u \in U) \to (\exists r \in R r \subseteq u \to \exists r \in R (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y))))$
39	26 38	mpd	$⊢ (φ \land u \in U) \to \exists r \in R (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
40		r19.37v	$⊢ \exists r \in R (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x r y \to F (x) s F (y))) \to (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
41	39 40	syl	$⊢ (φ \land u \in U) \to (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
42	41	rexlimdva	$⊢ φ \to (\exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
43	42	ad3antrrr	$⊢ (((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \land s \in S) \to (\exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
44	20 43	mpd	$⊢ (((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \land s \in S) \to \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y))$
45	44	ralrimiva	$⊢ ((φ \land F : X ⟶ Y) \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \to \forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y))$
46		ssfg	$⊢ R \in fBas (X \times X) \to R \subseteq (X \times X) filGen R$
47	5 46	syl	$⊢ φ \to R \subseteq (X \times X) filGen R$
48	47 1	sseqtrrdi	$⊢ φ \to R \subseteq U$
49		ssrexv	$⊢ R \subseteq U \to (\exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \to \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
50		breq	$⊢ r = u \to (x r y \leftrightarrow x u y)$
51	50	imbi1d	$⊢ r = u \to ((x r y \to F (x) s F (y)) \leftrightarrow (x u y \to F (x) s F (y)))$
52	51	2ralbidv	$⊢ r = u \to (\forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \leftrightarrow \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
53	52	cbvrexvw	$⊢ \exists r \in U \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \leftrightarrow \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))$
54	49 53	imbitrdi	$⊢ R \subseteq U \to (\exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
55	48 54	syl	$⊢ φ \to (\exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
56	55	ralimdv	$⊢ φ \to (\forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \to \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
57	56	adantr	$⊢ (φ \land F : X ⟶ Y) \to (\forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \to \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
58		nfv	$⊢ Ⅎ s (φ \land F : X ⟶ Y)$
59		nfra1	$⊢ Ⅎ s \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))$
60	58 59	nfan	$⊢ Ⅎ s ((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)))$
61		nfv	$⊢ Ⅎ s v \in V$
62	60 61	nfan	$⊢ Ⅎ s (((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V)$
63		rspa	$⊢ (\forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \land s \in S) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))$
64	63	ad5ant24	$⊢ (((((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \land s \in S) \land s \subseteq v) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))$
65		simp-4l	$⊢ (((((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \land s \in S) \land s \subseteq v) \to (φ \land F : X ⟶ Y)$
66		simplr	$⊢ (((((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \land s \in S) \land s \subseteq v) \to s \in S$
67		simpr	$⊢ (((((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \land s \in S) \land s \subseteq v) \to s \subseteq v$
68		ssbr	$⊢ s \subseteq v \to (F (x) s F (y) \to F (x) v F (y))$
69	68	adantl	$⊢ (((φ \land F : X ⟶ Y) \land s \in S) \land s \subseteq v) \to (F (x) s F (y) \to F (x) v F (y))$
70	69	imim2d	$⊢ (((φ \land F : X ⟶ Y) \land s \in S) \land s \subseteq v) \to ((x u y \to F (x) s F (y)) \to (x u y \to F (x) v F (y)))$
71	70	ralimdv	$⊢ (((φ \land F : X ⟶ Y) \land s \in S) \land s \subseteq v) \to (\forall y \in X (x u y \to F (x) s F (y)) \to \forall y \in X (x u y \to F (x) v F (y)))$
72	71	ralimdv	$⊢ (((φ \land F : X ⟶ Y) \land s \in S) \land s \subseteq v) \to (\forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall x \in X \forall y \in X (x u y \to F (x) v F (y)))$
73	72	reximdv	$⊢ (((φ \land F : X ⟶ Y) \land s \in S) \land s \subseteq v) \to (\exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y)))$
74	65 66 67 73	syl21anc	$⊢ (((((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \land s \in S) \land s \subseteq v) \to (\exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y)))$
75	64 74	mpd	$⊢ (((((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \land s \in S) \land s \subseteq v) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))$
76	6	ad3antrrr	$⊢ (((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \to S \in fBas (Y \times Y)$
77		simpr	$⊢ (((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \to v \in V$
78	77 2	eleqtrdi	$⊢ (((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \to v \in ((Y \times Y) filGen S)$
79		elfg	$⊢ S \in fBas (Y \times Y) \to (v \in ((Y \times Y) filGen S) \leftrightarrow (v \subseteq Y \times Y \land \exists s \in S s \subseteq v))$
80	79	simplbda	$⊢ (S \in fBas (Y \times Y) \land v \in ((Y \times Y) filGen S)) \to \exists s \in S s \subseteq v$
81	76 78 80	syl2anc	$⊢ (((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \to \exists s \in S s \subseteq v$
82	62 75 81	r19.29af	$⊢ (((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \land v \in V) \to \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))$
83	82	ralrimiva	$⊢ ((φ \land F : X ⟶ Y) \land \forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y))) \to \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))$
84	83	ex	$⊢ (φ \land F : X ⟶ Y) \to (\forall s \in S \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) s F (y)) \to \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y)))$
85	57 84	syld	$⊢ (φ \land F : X ⟶ Y) \to (\forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)) \to \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y)))$
86	85	imp	$⊢ ((φ \land F : X ⟶ Y) \land \forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y))) \to \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))$
87	45 86	impbida	$⊢ (φ \land F : X ⟶ Y) \to (\forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y)) \leftrightarrow \forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y)))$
88	87	pm5.32da	$⊢ φ \to ((F : X ⟶ Y \land \forall v \in V \exists u \in U \forall x \in X \forall y \in X (x u y \to F (x) v F (y))) \leftrightarrow (F : X ⟶ Y \land \forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y))))$
89	8 88	bitrd	$⊢ φ \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \forall s \in S \exists r \in R \forall x \in X \forall y \in X (x r y \to F (x) s F (y))))$

Metamath Proof Explorer

Theorem isucn2

Proof