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