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 𝑉 ) )