Metamath Proof Explorer


Theorem ucnprima

Description: The preimage by a uniformly continuous function F of an entourage W of Y is an entourage of X . Note of the definition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Hypotheses ucnprima.1 ( 𝜑𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
ucnprima.2 ( 𝜑𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
ucnprima.3 ( 𝜑𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
ucnprima.4 ( 𝜑𝑊𝑉 )
ucnprima.5 𝐺 = ( 𝑥𝑋 , 𝑦𝑋 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ )
Assertion ucnprima ( 𝜑 → ( 𝐺𝑊 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 ucnprima.1 ( 𝜑𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 ucnprima.2 ( 𝜑𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
3 ucnprima.3 ( 𝜑𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
4 ucnprima.4 ( 𝜑𝑊𝑉 )
5 ucnprima.5 𝐺 = ( 𝑥𝑋 , 𝑦𝑋 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ )
6 1 2 3 4 5 ucnima ( 𝜑 → ∃ 𝑟𝑈 ( 𝐺𝑟 ) ⊆ 𝑊 )
7 5 mpofun Fun 𝐺
8 ustssxp ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) )
9 1 8 sylan ( ( 𝜑𝑟𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) )
10 opex ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ∈ V
11 5 10 dmmpo dom 𝐺 = ( 𝑋 × 𝑋 )
12 9 11 sseqtrrdi ( ( 𝜑𝑟𝑈 ) → 𝑟 ⊆ dom 𝐺 )
13 funimass3 ( ( Fun 𝐺𝑟 ⊆ dom 𝐺 ) → ( ( 𝐺𝑟 ) ⊆ 𝑊𝑟 ⊆ ( 𝐺𝑊 ) ) )
14 7 12 13 sylancr ( ( 𝜑𝑟𝑈 ) → ( ( 𝐺𝑟 ) ⊆ 𝑊𝑟 ⊆ ( 𝐺𝑊 ) ) )
15 14 rexbidva ( 𝜑 → ( ∃ 𝑟𝑈 ( 𝐺𝑟 ) ⊆ 𝑊 ↔ ∃ 𝑟𝑈 𝑟 ⊆ ( 𝐺𝑊 ) ) )
16 6 15 mpbid ( 𝜑 → ∃ 𝑟𝑈 𝑟 ⊆ ( 𝐺𝑊 ) )
17 1 adantr ( ( 𝜑𝑟𝑈 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
18 simpr ( ( 𝜑𝑟𝑈 ) → 𝑟𝑈 )
19 cnvimass ( 𝐺𝑊 ) ⊆ dom 𝐺
20 19 11 sseqtri ( 𝐺𝑊 ) ⊆ ( 𝑋 × 𝑋 )
21 20 a1i ( ( 𝜑𝑟𝑈 ) → ( 𝐺𝑊 ) ⊆ ( 𝑋 × 𝑋 ) )
22 ustssel ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟𝑈 ∧ ( 𝐺𝑊 ) ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑟 ⊆ ( 𝐺𝑊 ) → ( 𝐺𝑊 ) ∈ 𝑈 ) )
23 17 18 21 22 syl3anc ( ( 𝜑𝑟𝑈 ) → ( 𝑟 ⊆ ( 𝐺𝑊 ) → ( 𝐺𝑊 ) ∈ 𝑈 ) )
24 23 rexlimdva ( 𝜑 → ( ∃ 𝑟𝑈 𝑟 ⊆ ( 𝐺𝑊 ) → ( 𝐺𝑊 ) ∈ 𝑈 ) )
25 16 24 mpd ( 𝜑 → ( 𝐺𝑊 ) ∈ 𝑈 )