Metamath Proof Explorer

Theorem cnindis

Description: Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnindis 
|- ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( J Cn { (/) , A } ) = ( A ^m X ) )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( x e. { (/) , A } -> ( x = (/) \/ x = A ) )
2 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
3 2 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> J e. Top )
4 0opn 
 |-  ( J e. Top -> (/) e. J )
5 3 4 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> (/) e. J )
6 imaeq2 
 |-  ( x = (/) -> ( `' f " x ) = ( `' f " (/) ) )
7 ima0 
 |-  ( `' f " (/) ) = (/)
8 6 7 eqtrdi 
 |-  ( x = (/) -> ( `' f " x ) = (/) )
9 8 eleq1d 
 |-  ( x = (/) -> ( ( `' f " x ) e. J <-> (/) e. J ) )
10 5 9 syl5ibrcom 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> ( x = (/) -> ( `' f " x ) e. J ) )
11 fimacnv 
 |-  ( f : X --> A -> ( `' f " A ) = X )
12 11 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> ( `' f " A ) = X )
13 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
14 13 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> X e. J )
15 12 14 eqeltrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> ( `' f " A ) e. J )
16 imaeq2 
 |-  ( x = A -> ( `' f " x ) = ( `' f " A ) )
17 16 eleq1d 
 |-  ( x = A -> ( ( `' f " x ) e. J <-> ( `' f " A ) e. J ) )
18 15 17 syl5ibrcom 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> ( x = A -> ( `' f " x ) e. J ) )
19 10 18 jaod 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> ( ( x = (/) \/ x = A ) -> ( `' f " x ) e. J ) )
20 1 19 syl5 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> ( x e. { (/) , A } -> ( `' f " x ) e. J ) )
21 20 ralrimiv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A e. V ) /\ f : X --> A ) -> A. x e. { (/) , A } ( `' f " x ) e. J )
22 21 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( f : X --> A -> A. x e. { (/) , A } ( `' f " x ) e. J ) )
23 22 pm4.71d 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( f : X --> A <-> ( f : X --> A /\ A. x e. { (/) , A } ( `' f " x ) e. J ) ) )
24 id 
 |-  ( A e. V -> A e. V )
25 elmapg 
 |-  ( ( A e. V /\ X e. J ) -> ( f e. ( A ^m X ) <-> f : X --> A ) )
26 24 13 25 syl2anr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( f e. ( A ^m X ) <-> f : X --> A ) )
27 indistopon 
 |-  ( A e. V -> { (/) , A } e. ( TopOn ` A ) )
28 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ { (/) , A } e. ( TopOn ` A ) ) -> ( f e. ( J Cn { (/) , A } ) <-> ( f : X --> A /\ A. x e. { (/) , A } ( `' f " x ) e. J ) ) )
29 27 28 sylan2 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( f e. ( J Cn { (/) , A } ) <-> ( f : X --> A /\ A. x e. { (/) , A } ( `' f " x ) e. J ) ) )
30 23 26 29 3bitr4rd 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( f e. ( J Cn { (/) , A } ) <-> f e. ( A ^m X ) ) )
31 30 eqrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( J Cn { (/) , A } ) = ( A ^m X ) )