cstucnd

Description: A constant function is uniformly continuous. Deduction form. Example 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017)

	Ref	Expression
Hypotheses	cstucnd.1	$⊢ φ \to U \in UnifOn (X)$
	cstucnd.2	$⊢ φ \to V \in UnifOn (Y)$
	cstucnd.3	$⊢ φ \to A \in Y$
Assertion	cstucnd	$⊢ φ \to X \times \{A\} \in (U uCn V)$

Proof

Step	Hyp	Ref	Expression
1		cstucnd.1	$⊢ φ \to U \in UnifOn (X)$
2		cstucnd.2	$⊢ φ \to V \in UnifOn (Y)$
3		cstucnd.3	$⊢ φ \to A \in Y$
4		fconst6g	$⊢ A \in Y \to (X \times \{A\}) : X ⟶ Y$
5	3 4	syl	$⊢ φ \to (X \times \{A\}) : X ⟶ Y$
6	1	adantr	$⊢ (φ \land s \in V) \to U \in UnifOn (X)$
7		ustne0	$⊢ U \in UnifOn (X) \to U \neq \emptyset$
8	6 7	syl	$⊢ (φ \land s \in V) \to U \neq \emptyset$
9	2	ad3antrrr	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to V \in UnifOn (Y)$
10		simpllr	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to s \in V$
11	3	ad3antrrr	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to A \in Y$
12		ustref	$⊢ (V \in UnifOn (Y) \land s \in V \land A \in Y) \to A s A$
13	9 10 11 12	syl3anc	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to A s A$
14		simprl	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to x \in X$
15		fvconst2g	$⊢ (A \in Y \land x \in X) \to (X \times \{A\}) (x) = A$
16	11 14 15	syl2anc	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to (X \times \{A\}) (x) = A$
17		simprr	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to y \in X$
18		fvconst2g	$⊢ (A \in Y \land y \in X) \to (X \times \{A\}) (y) = A$
19	11 17 18	syl2anc	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to (X \times \{A\}) (y) = A$
20	13 16 19	3brtr4d	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to (X \times \{A\}) (x) s (X \times \{A\}) (y)$
21	20	a1d	$⊢ (((φ \land s \in V) \land r \in U) \land (x \in X \land y \in X)) \to (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))$
22	21	ralrimivva	$⊢ ((φ \land s \in V) \land r \in U) \to \forall x \in X \forall y \in X (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))$
23	22	reximdva0	$⊢ ((φ \land s \in V) \land U \neq \emptyset) \to \exists r \in U \forall x \in X \forall y \in X (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))$
24	8 23	mpdan	$⊢ (φ \land s \in V) \to \exists r \in U \forall x \in X \forall y \in X (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))$
25	24	ralrimiva	$⊢ φ \to \forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))$
26		isucn	$⊢ (U \in UnifOn (X) \land V \in UnifOn (Y)) \to (X \times \{A\} \in (U uCn V) \leftrightarrow ((X \times \{A\}) : X ⟶ Y \land \forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))))$
27	1 2 26	syl2anc	$⊢ φ \to (X \times \{A\} \in (U uCn V) \leftrightarrow ((X \times \{A\}) : X ⟶ Y \land \forall s \in V \exists r \in U \forall x \in X \forall y \in X (x r y \to (X \times \{A\}) (x) s (X \times \{A\}) (y))))$
28	5 25 27	mpbir2and	$⊢ φ \to X \times \{A\} \in (U uCn V)$

Metamath Proof Explorer

Theorem cstucnd

Proof