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 ⊢ φ → U ∈ UnifOn ⁡ X
ucnprima.2 ⊢ φ → V ∈ UnifOn ⁡ Y
ucnprima.3 ⊢ φ → F ∈ U uCn V
ucnprima.4 ⊢ φ → W ∈ V
ucnprima.5 ⊢ G = x ∈ X , y ∈ X ⟼ F ⁡ x F ⁡ y
Assertion ucnprima ⊢ φ → G -1 W ∈ U

Proof

Step Hyp Ref Expression
1 ucnprima.1 ⊢ φ → U ∈ UnifOn ⁡ X
2 ucnprima.2 ⊢ φ → V ∈ UnifOn ⁡ Y
3 ucnprima.3 ⊢ φ → F ∈ U uCn V
4 ucnprima.4 ⊢ φ → W ∈ V
5 ucnprima.5 ⊢ G = x ∈ X , y ∈ X ⟼ F ⁡ x F ⁡ y
6 1 2 3 4 5 ucnima ⊢ φ → ∃ r ∈ U G r ⊆ W
7 5 mpofun ⊢ Fun ⁡ G
8 ustssxp ⊢ U ∈ UnifOn ⁡ X ∧ r ∈ U → r ⊆ X × X
9 1 8 sylan ⊢ φ ∧ r ∈ U → r ⊆ X × X
10 opex ⊢ F ⁡ x F ⁡ y ∈ V
11 5 10 dmmpo ⊢ dom ⁡ G = X × X
12 9 11 sseqtrrdi ⊢ φ ∧ r ∈ U → r ⊆ dom ⁡ G
13 funimass3 ⊢ Fun ⁡ G ∧ r ⊆ dom ⁡ G → G r ⊆ W ↔ r ⊆ G -1 W
14 7 12 13 sylancr ⊢ φ ∧ r ∈ U → G r ⊆ W ↔ r ⊆ G -1 W
15 14 rexbidva ⊢ φ → ∃ r ∈ U G r ⊆ W ↔ ∃ r ∈ U r ⊆ G -1 W
16 6 15 mpbid ⊢ φ → ∃ r ∈ U r ⊆ G -1 W
17 1 adantr ⊢ φ ∧ r ∈ U → U ∈ UnifOn ⁡ X
18 simpr ⊢ φ ∧ r ∈ U → r ∈ U
19 cnvimass ⊢ G -1 W ⊆ dom ⁡ G
20 19 11 sseqtri ⊢ G -1 W ⊆ X × X
21 20 a1i ⊢ φ ∧ r ∈ U → G -1 W ⊆ X × X
22 ustssel ⊢ U ∈ UnifOn ⁡ X ∧ r ∈ U ∧ G -1 W ⊆ X × X → r ⊆ G -1 W → G -1 W ∈ U
23 17 18 21 22 syl3anc ⊢ φ ∧ r ∈ U → r ⊆ G -1 W → G -1 W ∈ U
24 23 rexlimdva ⊢ φ → ∃ r ∈ U r ⊆ G -1 W → G -1 W ∈ U
25 16 24 mpd ⊢ φ → G -1 W ∈ U