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∈Fin↔𝒫A∈Comp

Proof

Step Hyp Ref Expression
1 distop ⊢A∈Fin→𝒫A∈Top
2 pwfi ⊢A∈Fin↔𝒫A∈Fin
3 2 biimpi ⊢A∈Fin→𝒫A∈Fin
4 1 3 elind ⊢A∈Fin→𝒫A∈Top∩Fin
5 fincmp ⊢𝒫A∈Top∩Fin→𝒫A∈Comp
6 4 5 syl ⊢A∈Fin→𝒫A∈Comp
7 simpr ⊢𝒫A∈Comp∧x∈A→x∈A
8 7 snssd ⊢𝒫A∈Comp∧x∈A→x⊆A
9 vsnex ⊢x∈V
10 9 elpw ⊢x∈𝒫A↔x⊆A
11 8 10 sylibr ⊢𝒫A∈Comp∧x∈A→x∈𝒫A
12 11 fmpttd ⊢𝒫A∈Comp→x∈A⟼x:A⟶𝒫A
13 12 frnd ⊢𝒫A∈Comp→ran⁡x∈A⟼x⊆𝒫A
14 eqid ⊢x∈A⟼x=x∈A⟼x
15 14 rnmpt ⊢ran⁡x∈A⟼x=y|∃x∈Ay=x
16 15 unieqi ⊢⋃ran⁡x∈A⟼x=⋃y|∃x∈Ay=x
17 9 dfiun2 ⊢⋃x∈Ax=⋃y|∃x∈Ay=x
18 iunid ⊢⋃x∈Ax=A
19 16 17 18 3eqtr2ri ⊢A=⋃ran⁡x∈A⟼x
20 19 a1i ⊢𝒫A∈Comp→A=⋃ran⁡x∈A⟼x
21 unipw ⊢⋃𝒫A=A
22 21 eqcomi ⊢A=⋃𝒫A
23 22 cmpcov ⊢𝒫A∈Comp∧ran⁡x∈A⟼x⊆𝒫A∧A=⋃ran⁡x∈A⟼x→∃y∈𝒫ran⁡x∈A⟼x∩FinA=⋃y
24 13 20 23 mpd3an23 ⊢𝒫A∈Comp→∃y∈𝒫ran⁡x∈A⟼x∩FinA=⋃y
25 elinel2 ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→y∈Fin
26 elinel1 ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→y∈𝒫ran⁡x∈A⟼x
27 26 elpwid ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→y⊆ran⁡x∈A⟼x
28 snfi ⊢x∈Fin
29 28 rgenw ⊢∀x∈Ax∈Fin
30 14 fmpt ⊢∀x∈Ax∈Fin↔x∈A⟼x:A⟶Fin
31 29 30 mpbi ⊢x∈A⟼x:A⟶Fin
32 frn ⊢x∈A⟼x:A⟶Fin→ran⁡x∈A⟼x⊆Fin
33 31 32 mp1i ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→ran⁡x∈A⟼x⊆Fin
34 27 33 sstrd ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→y⊆Fin
35 unifi ⊢y∈Fin∧y⊆Fin→⋃y∈Fin
36 25 34 35 syl2anc ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→⋃y∈Fin
37 eleq1 ⊢A=⋃y→A∈Fin↔⋃y∈Fin
38 36 37 syl5ibrcom ⊢y∈𝒫ran⁡x∈A⟼x∩Fin→A=⋃y→A∈Fin
39 38 rexlimiv ⊢∃y∈𝒫ran⁡x∈A⟼x∩FinA=⋃y→A∈Fin
40 24 39 syl ⊢𝒫A∈Comp→A∈Fin
41 6 40 impbii ⊢A∈Fin↔𝒫A∈Comp