Metamath Proof Explorer

Theorem isucn

Description: The predicate " F is a uniformly continuous function from uniform space U to uniform space V ". (Contributed by Thierry Arnoux, 16-Nov-2017)

		Ref	Expression
	Assertion	isucn	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \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		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))\}$
2	1	eleq2d	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow F \in \{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))\})$
3		fveq1	$⊢ f = F \to f (x) = F (x)$
4		fveq1	$⊢ f = F \to f (y) = F (y)$
5	3 4	breq12d	$⊢ f = F \to (f (x) s f (y) \leftrightarrow F (x) s F (y))$
6	5	imbi2d	$⊢ f = F \to ((x r y \to f (x) s f (y)) \leftrightarrow (x r y \to F (x) s F (y)))$
7	6	ralbidv	$⊢ f = F \to (\forall y \in X (x r y \to f (x) s f (y)) \leftrightarrow \forall y \in X (x r y \to F (x) s F (y)))$
8	7	rexralbidv	$⊢ f = F \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 X \forall y \in X (x r y \to F (x) s F (y)))$
9	8	ralbidv	$⊢ f = F \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 X \forall y \in X (x r y \to F (x) s F (y)))$
10	9	elrab	$⊢ F \in \{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))\} \leftrightarrow (F \in (Y^{X}) \land \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)))$
11	2 10	bitrdi	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow (F \in (Y^{X}) \land \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))))$
12		elfvex	$⊢ V \in UnifOn (Y) \to Y \in V$
13		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
14		elmapg	$⊢ (Y \in V \land X \in V) \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
15	12 13 14	syl2anr	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
16	15	anbi1d	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to ((F \in (Y^{X}) \land \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 (F : X ⟶ Y \land \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))))$
17	11 16	bitrd	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (F \in (U uCn V) \leftrightarrow (F : X ⟶ Y \land \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))))$