Metamath Proof Explorer

Theorem cnconst2

Description: A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion cnconst2 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 fconst6g 
 |-  ( B e. Y -> ( X X. { B } ) : X --> Y )
2 1 3ad2ant3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) : X --> Y )
3 2 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> ( X X. { B } ) : X --> Y )
4 simpll3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> B e. Y )
5 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> x e. X )
6 fvconst2g 
 |-  ( ( B e. Y /\ x e. X ) -> ( ( X X. { B } ) ` x ) = B )
7 4 5 6 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( ( X X. { B } ) ` x ) = B )
8 7 eleq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( ( ( X X. { B } ) ` x ) e. y <-> B e. y ) )
9 simpll1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> J e. ( TopOn ` X ) )
10 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
11 9 10 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> X e. J )
12 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> x e. X )
13 df-ima 
 |-  ( ( X X. { B } ) " X ) = ran ( ( X X. { B } ) |` X )
14 ssid 
 |-  X C_ X
15 xpssres 
 |-  ( X C_ X -> ( ( X X. { B } ) |` X ) = ( X X. { B } ) )
16 14 15 ax-mp 
 |-  ( ( X X. { B } ) |` X ) = ( X X. { B } )
17 16 rneqi 
 |-  ran ( ( X X. { B } ) |` X ) = ran ( X X. { B } )
18 rnxpss 
 |-  ran ( X X. { B } ) C_ { B }
19 17 18 eqsstri 
 |-  ran ( ( X X. { B } ) |` X ) C_ { B }
20 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> B e. y )
21 20 snssd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> { B } C_ y )
22 19 21 sstrid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> ran ( ( X X. { B } ) |` X ) C_ y )
23 13 22 eqsstrid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> ( ( X X. { B } ) " X ) C_ y )
24 eleq2 
 |-  ( u = X -> ( x e. u <-> x e. X ) )
25 imaeq2 
 |-  ( u = X -> ( ( X X. { B } ) " u ) = ( ( X X. { B } ) " X ) )
26 25 sseq1d 
 |-  ( u = X -> ( ( ( X X. { B } ) " u ) C_ y <-> ( ( X X. { B } ) " X ) C_ y ) )
27 24 26 anbi12d 
 |-  ( u = X -> ( ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) <-> ( x e. X /\ ( ( X X. { B } ) " X ) C_ y ) ) )
28 27 rspcev 
 |-  ( ( X e. J /\ ( x e. X /\ ( ( X X. { B } ) " X ) C_ y ) ) -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) )
29 11 12 23 28 syl12anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) )
30 29 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( B e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) )
31 8 30 sylbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) )
32 31 ralrimiva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> A. y e. K ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) )
33 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> J e. ( TopOn ` X ) )
34 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> K e. ( TopOn ` Y ) )
35 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> x e. X )
36 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ x e. X ) -> ( ( X X. { B } ) e. ( ( J CnP K ) ` x ) <-> ( ( X X. { B } ) : X --> Y /\ A. y e. K ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) ) )
37 33 34 35 36 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> ( ( X X. { B } ) e. ( ( J CnP K ) ` x ) <-> ( ( X X. { B } ) : X --> Y /\ A. y e. K ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) ) )
38 3 32 37 mpbir2and 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> ( X X. { B } ) e. ( ( J CnP K ) ` x ) )
39 38 ralrimiva 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> A. x e. X ( X X. { B } ) e. ( ( J CnP K ) ` x ) )
40 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( X X. { B } ) e. ( J Cn K ) <-> ( ( X X. { B } ) : X --> Y /\ A. x e. X ( X X. { B } ) e. ( ( J CnP K ) ` x ) ) ) )
41 40 3adant3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( ( X X. { B } ) e. ( J Cn K ) <-> ( ( X X. { B } ) : X --> Y /\ A. x e. X ( X X. { B } ) e. ( ( J CnP K ) ` x ) ) ) )
42 2 39 41 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) )