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 
|- ( ph -> U e. ( UnifOn ` X ) )
cstucnd.2 
|- ( ph -> V e. ( UnifOn ` Y ) )
cstucnd.3 
|- ( ph -> A e. Y )
Assertion cstucnd 
|- ( ph -> ( X X. { A } ) e. ( U uCn V ) )

Proof

Step Hyp Ref Expression
1 cstucnd.1 
 |-  ( ph -> U e. ( UnifOn ` X ) )
2 cstucnd.2 
 |-  ( ph -> V e. ( UnifOn ` Y ) )
3 cstucnd.3 
 |-  ( ph -> A e. Y )
4 fconst6g 
 |-  ( A e. Y -> ( X X. { A } ) : X --> Y )
5 3 4 syl 
 |-  ( ph -> ( X X. { A } ) : X --> Y )
6 1 adantr 
 |-  ( ( ph /\ s e. V ) -> U e. ( UnifOn ` X ) )
7 ustne0 
 |-  ( U e. ( UnifOn ` X ) -> U =/= (/) )
8 6 7 syl 
 |-  ( ( ph /\ s e. V ) -> U =/= (/) )
9 2 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> V e. ( UnifOn ` Y ) )
10 simpllr 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> s e. V )
11 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> A e. Y )
12 ustref 
 |-  ( ( V e. ( UnifOn ` Y ) /\ s e. V /\ A e. Y ) -> A s A )
13 9 10 11 12 syl3anc 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> A s A )
14 simprl 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> x e. X )
15 fvconst2g 
 |-  ( ( A e. Y /\ x e. X ) -> ( ( X X. { A } ) ` x ) = A )
16 11 14 15 syl2anc 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( ( X X. { A } ) ` x ) = A )
17 simprr 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> y e. X )
18 fvconst2g 
 |-  ( ( A e. Y /\ y e. X ) -> ( ( X X. { A } ) ` y ) = A )
19 11 17 18 syl2anc 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( ( X X. { A } ) ` y ) = A )
20 13 16 19 3brtr4d 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) )
21 20 a1d 
 |-  ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) )
22 21 ralrimivva 
 |-  ( ( ( ph /\ s e. V ) /\ r e. U ) -> A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) )
23 22 reximdva0 
 |-  ( ( ( ph /\ s e. V ) /\ U =/= (/) ) -> E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) )
24 8 23 mpdan 
 |-  ( ( ph /\ s e. V ) -> E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) )
25 24 ralrimiva 
 |-  ( ph -> A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) )
26 isucn 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( ( X X. { A } ) e. ( U uCn V ) <-> ( ( X X. { A } ) : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) ) )
27 1 2 26 syl2anc 
 |-  ( ph -> ( ( X X. { A } ) e. ( U uCn V ) <-> ( ( X X. { A } ) : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) ) )
28 5 25 27 mpbir2and 
 |-  ( ph -> ( X X. { A } ) e. ( U uCn V ) )