Metamath Proof Explorer

Theorem cndis

Description: Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cndis 
|- ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( ~P A Cn J ) = ( X ^m A ) )

Proof

Step Hyp Ref Expression
1 cnvimass 
 |-  ( `' f " x ) C_ dom f
2 fdm 
 |-  ( f : A --> X -> dom f = A )
3 2 adantl 
 |-  ( ( ( A e. V /\ J e. ( TopOn ` X ) ) /\ f : A --> X ) -> dom f = A )
4 1 3 sseqtrid 
 |-  ( ( ( A e. V /\ J e. ( TopOn ` X ) ) /\ f : A --> X ) -> ( `' f " x ) C_ A )
5 elpw2g 
 |-  ( A e. V -> ( ( `' f " x ) e. ~P A <-> ( `' f " x ) C_ A ) )
6 5 ad2antrr 
 |-  ( ( ( A e. V /\ J e. ( TopOn ` X ) ) /\ f : A --> X ) -> ( ( `' f " x ) e. ~P A <-> ( `' f " x ) C_ A ) )
7 4 6 mpbird 
 |-  ( ( ( A e. V /\ J e. ( TopOn ` X ) ) /\ f : A --> X ) -> ( `' f " x ) e. ~P A )
8 7 ralrimivw 
 |-  ( ( ( A e. V /\ J e. ( TopOn ` X ) ) /\ f : A --> X ) -> A. x e. J ( `' f " x ) e. ~P A )
9 8 ex 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( f : A --> X -> A. x e. J ( `' f " x ) e. ~P A ) )
10 9 pm4.71d 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( f : A --> X <-> ( f : A --> X /\ A. x e. J ( `' f " x ) e. ~P A ) ) )
11 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
12 id 
 |-  ( A e. V -> A e. V )
13 elmapg 
 |-  ( ( X e. J /\ A e. V ) -> ( f e. ( X ^m A ) <-> f : A --> X ) )
14 11 12 13 syl2anr 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( f e. ( X ^m A ) <-> f : A --> X ) )
15 distopon 
 |-  ( A e. V -> ~P A e. ( TopOn ` A ) )
16 iscn 
 |-  ( ( ~P A e. ( TopOn ` A ) /\ J e. ( TopOn ` X ) ) -> ( f e. ( ~P A Cn J ) <-> ( f : A --> X /\ A. x e. J ( `' f " x ) e. ~P A ) ) )
17 15 16 sylan 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( f e. ( ~P A Cn J ) <-> ( f : A --> X /\ A. x e. J ( `' f " x ) e. ~P A ) ) )
18 10 14 17 3bitr4rd 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( f e. ( ~P A Cn J ) <-> f e. ( X ^m A ) ) )
19 18 eqrdv 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( ~P A Cn J ) = ( X ^m A ) )