Metamath Proof Explorer

Theorem discmp

Description: A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion discmp 
|- ( A e. Fin <-> ~P A e. Comp )

Proof

Step Hyp Ref Expression
1 distop 
 |-  ( A e. Fin -> ~P A e. Top )
2 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
3 2 biimpi 
 |-  ( A e. Fin -> ~P A e. Fin )
4 1 3 elind 
 |-  ( A e. Fin -> ~P A e. ( Top i^i Fin ) )
5 fincmp 
 |-  ( ~P A e. ( Top i^i Fin ) -> ~P A e. Comp )
6 4 5 syl 
 |-  ( A e. Fin -> ~P A e. Comp )
7 simpr 
 |-  ( ( ~P A e. Comp /\ x e. A ) -> x e. A )
8 7 snssd 
 |-  ( ( ~P A e. Comp /\ x e. A ) -> { x } C_ A )
9 snex 
 |-  { x } e. _V
10 9 elpw 
 |-  ( { x } e. ~P A <-> { x } C_ A )
11 8 10 sylibr 
 |-  ( ( ~P A e. Comp /\ x e. A ) -> { x } e. ~P A )
12 11 fmpttd 
 |-  ( ~P A e. Comp -> ( x e. A |-> { x } ) : A --> ~P A )
13 12 frnd 
 |-  ( ~P A e. Comp -> ran ( x e. A |-> { x } ) C_ ~P A )
14 eqid 
 |-  ( x e. A |-> { x } ) = ( x e. A |-> { x } )
15 14 rnmpt 
 |-  ran ( x e. A |-> { x } ) = { y | E. x e. A y = { x } }
16 15 unieqi 
 |-  U. ran ( x e. A |-> { x } ) = U. { y | E. x e. A y = { x } }
17 9 dfiun2 
 |-  U_ x e. A { x } = U. { y | E. x e. A y = { x } }
18 iunid 
 |-  U_ x e. A { x } = A
19 16 17 18 3eqtr2ri 
 |-  A = U. ran ( x e. A |-> { x } )
20 19 a1i 
 |-  ( ~P A e. Comp -> A = U. ran ( x e. A |-> { x } ) )
21 unipw 
 |-  U. ~P A = A
22 21 eqcomi 
 |-  A = U. ~P A
23 22 cmpcov 
 |-  ( ( ~P A e. Comp /\ ran ( x e. A |-> { x } ) C_ ~P A /\ A = U. ran ( x e. A |-> { x } ) ) -> E. y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) A = U. y )
24 13 20 23 mpd3an23 
 |-  ( ~P A e. Comp -> E. y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) A = U. y )
25 elinel2 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> y e. Fin )
26 elinel1 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> y e. ~P ran ( x e. A |-> { x } ) )
27 26 elpwid 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> y C_ ran ( x e. A |-> { x } ) )
28 snfi 
 |-  { x } e. Fin
29 28 rgenw 
 |-  A. x e. A { x } e. Fin
30 14 fmpt 
 |-  ( A. x e. A { x } e. Fin <-> ( x e. A |-> { x } ) : A --> Fin )
31 29 30 mpbi 
 |-  ( x e. A |-> { x } ) : A --> Fin
32 frn 
 |-  ( ( x e. A |-> { x } ) : A --> Fin -> ran ( x e. A |-> { x } ) C_ Fin )
33 31 32 mp1i 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> ran ( x e. A |-> { x } ) C_ Fin )
34 27 33 sstrd 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> y C_ Fin )
35 unifi 
 |-  ( ( y e. Fin /\ y C_ Fin ) -> U. y e. Fin )
36 25 34 35 syl2anc 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> U. y e. Fin )
37 eleq1 
 |-  ( A = U. y -> ( A e. Fin <-> U. y e. Fin ) )
38 36 37 syl5ibrcom 
 |-  ( y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) -> ( A = U. y -> A e. Fin ) )
39 38 rexlimiv 
 |-  ( E. y e. ( ~P ran ( x e. A |-> { x } ) i^i Fin ) A = U. y -> A e. Fin )
40 24 39 syl 
 |-  ( ~P A e. Comp -> A e. Fin )
41 6 40 impbii 
 |-  ( A e. Fin <-> ~P A e. Comp )