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		snex	⊢ { 𝑥 } ∈ 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 )