Metamath Proof Explorer

Theorem isucn

Description: The predicate " F is a uniformly continuous function from uniform space U to uniform space V ". (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion isucn ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → F ∈ U uCn V ↔ F : X ⟶ Y ∧ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y

Proof

Step Hyp Ref Expression
1 ucnval ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → U uCn V = f ∈ Y X | ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → f ⁡ x s f ⁡ y
2 1 eleq2d ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → F ∈ U uCn V ↔ F ∈ f ∈ Y X | ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → f ⁡ x s f ⁡ y
3 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
4 fveq1 ⊢ f = F → f ⁡ y = F ⁡ y
5 3 4 breq12d ⊢ f = F → f ⁡ x s f ⁡ y ↔ F ⁡ x s F ⁡ y
6 5 imbi2d ⊢ f = F → x r y → f ⁡ x s f ⁡ y ↔ x r y → F ⁡ x s F ⁡ y
7 6 ralbidv ⊢ f = F → ∀ y ∈ X x r y → f ⁡ x s f ⁡ y ↔ ∀ y ∈ X x r y → F ⁡ x s F ⁡ y
8 7 rexralbidv ⊢ f = F → ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → f ⁡ x s f ⁡ y ↔ ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y
9 8 ralbidv ⊢ f = F → ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → f ⁡ x s f ⁡ y ↔ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y
10 9 elrab ⊢ F ∈ f ∈ Y X | ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → f ⁡ x s f ⁡ y ↔ F ∈ Y X ∧ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y
11 2 10 bitrdi ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → F ∈ U uCn V ↔ F ∈ Y X ∧ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y
12 elfvex ⊢ V ∈ UnifOn ⁡ Y → Y ∈ V
13 elfvex ⊢ U ∈ UnifOn ⁡ X → X ∈ V
14 elmapg ⊢ Y ∈ V ∧ X ∈ V → F ∈ Y X ↔ F : X ⟶ Y
15 12 13 14 syl2anr ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → F ∈ Y X ↔ F : X ⟶ Y
16 15 anbi1d ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → F ∈ Y X ∧ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y ↔ F : X ⟶ Y ∧ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y
17 11 16 bitrd ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ UnifOn ⁡ Y → F ∈ U uCn V ↔ F : X ⟶ Y ∧ ∀ s ∈ V ∃ r ∈ U ∀ x ∈ X ∀ y ∈ X x r y → F ⁡ x s F ⁡ y