Metamath Proof Explorer

Theorem iducn

Description: The identity is uniformly continuous from a uniform structure to itself. Example 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017)

		Ref	Expression
	Assertion	iducn	$⊢ U \in UnifOn (X) \to {I ↾}_{X} \in (U uCn U)$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{X}) : X \underset{1-1 onto}{⟶} X$
2		f1of	$⊢ ({I ↾}_{X}) : X \underset{1-1 onto}{⟶} X \to ({I ↾}_{X}) : X ⟶ X$
3	1 2	mp1i	$⊢ U \in UnifOn (X) \to ({I ↾}_{X}) : X ⟶ X$
4		simpr	$⊢ (U \in UnifOn (X) \land s \in U) \to s \in U$
5		fvresi	$⊢ x \in X \to ({I ↾}_{X}) (x) = x$
6		fvresi	$⊢ y \in X \to ({I ↾}_{X}) (y) = y$
7	5 6	breqan12d	$⊢ (x \in X \land y \in X) \to (({I ↾}_{X}) (x) s ({I ↾}_{X}) (y) \leftrightarrow x s y)$
8	7	biimprd	$⊢ (x \in X \land y \in X) \to (x s y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))$
9	8	adantl	$⊢ ((U \in UnifOn (X) \land s \in U) \land (x \in X \land y \in X)) \to (x s y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))$
10	9	ralrimivva	$⊢ (U \in UnifOn (X) \land s \in U) \to \forall x \in X \forall y \in X (x s y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))$
11		breq	$⊢ r = s \to (x r y \leftrightarrow x s y)$
12	11	imbi1d	$⊢ r = s \to ((x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y)) \leftrightarrow (x s y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y)))$
13	12	2ralbidv	$⊢ r = s \to (\forall x \in X \forall y \in X (x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y)) \leftrightarrow \forall x \in X \forall y \in X (x s y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y)))$
14	13	rspcev	$⊢ (s \in U \land \forall x \in X \forall y \in X (x s y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))) \to \exists r \in U \forall x \in X \forall y \in X (x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))$
15	4 10 14	syl2anc	$⊢ (U \in UnifOn (X) \land s \in U) \to \exists r \in U \forall x \in X \forall y \in X (x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))$
16	15	ralrimiva	$⊢ U \in UnifOn (X) \to \forall s \in U \exists r \in U \forall x \in X \forall y \in X (x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))$
17		isucn	$⊢ (U \in UnifOn (X) \land U \in UnifOn (X)) \to ({I ↾}_{X} \in (U uCn U) \leftrightarrow (({I ↾}_{X}) : X ⟶ X \land \forall s \in U \exists r \in U \forall x \in X \forall y \in X (x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))))$
18	17	anidms	$⊢ U \in UnifOn (X) \to ({I ↾}_{X} \in (U uCn U) \leftrightarrow (({I ↾}_{X}) : X ⟶ X \land \forall s \in U \exists r \in U \forall x \in X \forall y \in X (x r y \to ({I ↾}_{X}) (x) s ({I ↾}_{X}) (y))))$
19	3 16 18	mpbir2and	$⊢ U \in UnifOn (X) \to {I ↾}_{X} \in (U uCn U)$