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 \in Fin \leftrightarrow 𝒫 A \in Comp$

Proof

Step	Hyp	Ref	Expression
1		distop	$⊢ A \in Fin \to 𝒫 A \in Top$
2		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
3	2	biimpi	$⊢ A \in Fin \to 𝒫 A \in Fin$
4	1 3	elind	$⊢ A \in Fin \to 𝒫 A \in (Top \cap Fin)$
5		fincmp	$⊢ 𝒫 A \in (Top \cap Fin) \to 𝒫 A \in Comp$
6	4 5	syl	$⊢ A \in Fin \to 𝒫 A \in Comp$
7		simpr	$⊢ (𝒫 A \in Comp \land x \in A) \to x \in A$
8	7	snssd	$⊢ (𝒫 A \in Comp \land x \in A) \to \{x\} \subseteq A$
9		vsnex	$⊢ \{x\} \in V$
10	9	elpw	$⊢ \{x\} \in 𝒫 A \leftrightarrow \{x\} \subseteq A$
11	8 10	sylibr	$⊢ (𝒫 A \in Comp \land x \in A) \to \{x\} \in 𝒫 A$
12	11	fmpttd	$⊢ 𝒫 A \in Comp \to (x \in A ⟼ \{x\}) : A ⟶ 𝒫 A$
13	12	frnd	$⊢ 𝒫 A \in Comp \to ran (x \in A ⟼ \{x\}) \subseteq 𝒫 A$
14		eqid	$⊢ (x \in A ⟼ \{x\}) = (x \in A ⟼ \{x\})$
15	14	rnmpt	$⊢ ran (x \in A ⟼ \{x\}) = \{y \| \exists x \in A y = \{x\}\}$
16	15	unieqi	$⊢ ⋃ ran (x \in A ⟼ \{x\}) = ⋃ \{y \| \exists x \in A y = \{x\}\}$
17	9	dfiun2	$⊢ ⋃_{x \in A} \{x\} = ⋃ \{y \| \exists x \in A y = \{x\}\}$
18		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
19	16 17 18	3eqtr2ri	$⊢ A = ⋃ ran (x \in A ⟼ \{x\})$
20	19	a1i	$⊢ 𝒫 A \in Comp \to A = ⋃ ran (x \in A ⟼ \{x\})$
21		unipw	$⊢ ⋃ 𝒫 A = A$
22	21	eqcomi	$⊢ A = ⋃ 𝒫 A$
23	22	cmpcov	$⊢ (𝒫 A \in Comp \land ran (x \in A ⟼ \{x\}) \subseteq 𝒫 A \land A = ⋃ ran (x \in A ⟼ \{x\})) \to \exists y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) A = ⋃ y$
24	13 20 23	mpd3an23	$⊢ 𝒫 A \in Comp \to \exists y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) A = ⋃ y$
25		elinel2	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to y \in Fin$
26		elinel1	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to y \in 𝒫 ran (x \in A ⟼ \{x\})$
27	26	elpwid	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to y \subseteq ran (x \in A ⟼ \{x\})$
28		snfi	$⊢ \{x\} \in Fin$
29	28	rgenw	$⊢ \forall x \in A \{x\} \in Fin$
30	14	fmpt	$⊢ \forall x \in A \{x\} \in Fin \leftrightarrow (x \in A ⟼ \{x\}) : A ⟶ Fin$
31	29 30	mpbi	$⊢ (x \in A ⟼ \{x\}) : A ⟶ Fin$
32		frn	$⊢ (x \in A ⟼ \{x\}) : A ⟶ Fin \to ran (x \in A ⟼ \{x\}) \subseteq Fin$
33	31 32	mp1i	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to ran (x \in A ⟼ \{x\}) \subseteq Fin$
34	27 33	sstrd	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to y \subseteq Fin$
35		unifi	$⊢ (y \in Fin \land y \subseteq Fin) \to ⋃ y \in Fin$
36	25 34 35	syl2anc	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to ⋃ y \in Fin$
37		eleq1	$⊢ A = ⋃ y \to (A \in Fin \leftrightarrow ⋃ y \in Fin)$
38	36 37	syl5ibrcom	$⊢ y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) \to (A = ⋃ y \to A \in Fin)$
39	38	rexlimiv	$⊢ \exists y \in (𝒫 ran (x \in A ⟼ \{x\}) \cap Fin) A = ⋃ y \to A \in Fin$
40	24 39	syl	$⊢ 𝒫 A \in Comp \to A \in Fin$
41	6 40	impbii	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Comp$

Metamath Proof Explorer

Theorem discmp

Proof