ucnval

Description: The set of all uniformly continuous function from uniform space U to uniform space V . (Contributed by Thierry Arnoux, 16-Nov-2017)

		Ref	Expression
	Assertion	ucnval	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to U uCn V = \{f \in (Y^{X}) \| \forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to f (x) s f (y))\}$

Proof

Step	Hyp	Ref	Expression
1		elrnust	$⊢ U \in UnifOn (X) \to U \in ⋃ ran UnifOn$
2	1	adantr	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to U \in ⋃ ran UnifOn$
3		elrnust	$⊢ V \in UnifOn (Y) \to V \in ⋃ ran UnifOn$
4	3	adantl	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to V \in ⋃ ran UnifOn$
5		ovex	$⊢ {dom ⋃ V}^{dom ⋃ U} \in V$
6	5	rabex	$⊢ \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\} \in V$
7	6	a1i	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\} \in V$
8		simpr	$⊢ (u = U \land v = V) \to v = V$
9	8	unieqd	$⊢ (u = U \land v = V) \to ⋃ v = ⋃ V$
10	9	dmeqd	$⊢ (u = U \land v = V) \to dom ⋃ v = dom ⋃ V$
11		simpl	$⊢ (u = U \land v = V) \to u = U$
12	11	unieqd	$⊢ (u = U \land v = V) \to ⋃ u = ⋃ U$
13	12	dmeqd	$⊢ (u = U \land v = V) \to dom ⋃ u = dom ⋃ U$
14	10 13	oveq12d	$⊢ (u = U \land v = V) \to {dom ⋃ v}^{dom ⋃ u} = {dom ⋃ V}^{dom ⋃ U}$
15	13	raleqdv	$⊢ (u = U \land v = V) \to (\forall y \in dom ⋃ u (x r y \to f (x) s f (y)) \leftrightarrow \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
16	13 15	raleqbidv	$⊢ (u = U \land v = V) \to (\forall x \in dom ⋃ u \forall y \in dom ⋃ u (x r y \to f (x) s f (y)) \leftrightarrow \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
17	11 16	rexeqbidv	$⊢ (u = U \land v = V) \to (\exists r \in u \forall x \in dom ⋃ u \forall y \in dom ⋃ u (x r y \to f (x) s f (y)) \leftrightarrow \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
18	8 17	raleqbidv	$⊢ (u = U \land v = V) \to (\forall s \in v \exists r \in u \forall x \in dom ⋃ u \forall y \in dom ⋃ u (x r y \to f (x) s f (y)) \leftrightarrow \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
19	14 18	rabeqbidv	$⊢ (u = U \land v = V) \to \{f \in ({dom ⋃ v}^{dom ⋃ u}) \| \forall s \in v \exists r \in u \forall x \in dom ⋃ u \forall y \in dom ⋃ u (x r y \to f (x) s f (y))\} = \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\}$
20		df-ucn	$⊢ uCn = (u \in ⋃ ran UnifOn, v \in ⋃ ran UnifOn ⟼ \{f \in ({dom ⋃ v}^{dom ⋃ u}) \| \forall s \in v \exists r \in u \forall x \in dom ⋃ u \forall y \in dom ⋃ u (x r y \to f (x) s f (y))\})$
21	19 20	ovmpoga	$⊢ (U \in ⋃ ran UnifOn \land V \in ⋃ ran UnifOn \land \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\} \in V) \to U uCn V = \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\}$
22	2 4 7 21	syl3anc	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to U uCn V = \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\}$
23		ustbas2	$⊢ V \in UnifOn (Y) \to Y = dom ⋃ V$
24		ustbas2	$⊢ U \in UnifOn (X) \to X = dom ⋃ U$
25	23 24	oveqan12rd	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to Y^{X} = {dom ⋃ V}^{dom ⋃ U}$
26	24	adantr	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to X = dom ⋃ U$
27	26	raleqdv	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (\forall y \in X (x r y \to f (x) s f (y)) \leftrightarrow \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
28	26 27	raleqbidv	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (\forall x \in X \forall y \in X (x r y \to f (x) s f (y)) \leftrightarrow \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
29	28	rexbidv	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (\exists r \in U \forall x \in X \forall y \in X (x r y \to f (x) s f (y)) \leftrightarrow \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
30	29	ralbidv	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (\forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to f (x) s f (y)) \leftrightarrow \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y)))$
31	25 30	rabeqbidv	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to \{f \in (Y^{X}) \| \forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to f (x) s f (y))\} = \{f \in ({dom ⋃ V}^{dom ⋃ U}) \| \forall s \in V \exists r \in U \forall x \in dom ⋃ U \forall y \in dom ⋃ U (x r y \to f (x) s f (y))\}$
32	22 31	eqtr4d	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to U uCn V = \{f \in (Y^{X}) \| \forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to f (x) s f (y))\}$

Metamath Proof Explorer

Theorem ucnval

Proof