This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Comp )

Proof

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