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 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝑈 Cnu 𝑈 ) )

Proof

Step Hyp Ref Expression
1 f1oi ⊢ ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋
2 f1of ⊢ ( ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 → ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 )
3 1 2 mp1i ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 )
4 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ∈ 𝑈 )
5 fvresi ⊢ ( 𝑥 ∈ 𝑋 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) = 𝑥 )
6 fvresi ⊢ ( 𝑦 ∈ 𝑋 → ( ( I ↾ 𝑋 ) ‘ 𝑦 ) = 𝑦 )
7 5 6 breqan12d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ↔ 𝑥 𝑠 𝑦 ) )
8 7 biimprd ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑠 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) )
9 8 adantl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑠 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) )
10 9 ralrimivva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑠 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) )
11 breq ⊢ ( 𝑟 = 𝑠 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑠 𝑦 ) )
12 11 imbi1d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ( 𝑥 𝑠 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
13 12 2ralbidv ⊢ ( 𝑟 = 𝑠 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑠 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
14 13 rspcev ⊢ ( ( 𝑠 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑠 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) )
15 4 10 14 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) )
16 15 ralrimiva ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) )
17 isucn ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝑈 Cnu 𝑈 ) ↔ ( ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 ∧ ∀ 𝑠 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) )
18 17 anidms ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( I ↾ 𝑋 ) ∈ ( 𝑈 Cnu 𝑈 ) ↔ ( ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 ∧ ∀ 𝑠 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( I ↾ 𝑋 ) ‘ 𝑥 ) 𝑠 ( ( I ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) )
19 3 16 18 mpbir2and ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝑈 Cnu 𝑈 ) )