This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cstucnd

Description: A constant function is uniformly continuous. Deduction form. Example 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Hypotheses cstucnd.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
cstucnd.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
cstucnd.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑌 )
Assertion cstucnd ( 𝜑 → ( 𝑋 × { 𝐴 } ) ∈ ( 𝑈 Cnu 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cstucnd.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 cstucnd.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
3 cstucnd.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑌 )
4 fconst6g ⊢ ( 𝐴 ∈ 𝑌 → ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ 𝑌 )
5 3 4 syl ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ 𝑌 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
7 ustne0 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ≠ ∅ )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) → 𝑈 ≠ ∅ )
9 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
10 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑠 ∈ 𝑉 )
11 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑌 )
12 ustref ⊢ ( ( 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ∧ 𝑠 ∈ 𝑉 ∧ 𝐴 ∈ 𝑌 ) → 𝐴 𝑠 𝐴 )
13 9 10 11 12 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐴 𝑠 𝐴 )
14 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
15 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
16 11 14 15 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
17 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
18 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) = 𝐴 )
19 11 17 18 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) = 𝐴 )
20 13 16 19 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) )
21 20 a1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) )
22 21 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) )
23 22 reximdva0 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) ∧ 𝑈 ≠ ∅ ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) )
24 8 23 mpdan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑉 ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) )
25 24 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) )
26 isucn ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ( 𝑋 × { 𝐴 } ) ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) ) ) )
27 1 2 26 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 × { 𝐴 } ) ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) 𝑠 ( ( 𝑋 × { 𝐴 } ) ‘ 𝑦 ) ) ) ) )
28 5 25 27 mpbir2and ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) ∈ ( 𝑈 Cnu 𝑉 ) )