cmpcov

Description: An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009)

		Ref	Expression
	Hypothesis	iscmp.1	$⊢ X = ⋃ J$
	Assertion	cmpcov	$⊢ (J \in Comp \land S \subseteq J \land X = ⋃ S) \to \exists s \in (𝒫 S \cap Fin) X = ⋃ s$

Step	Hyp	Ref	Expression
1		iscmp.1	$⊢ X = ⋃ J$
2		unieq	$⊢ r = S \to ⋃ r = ⋃ S$
3	2	eqeq2d	$⊢ r = S \to (X = ⋃ r \leftrightarrow X = ⋃ S)$
4		pweq	$⊢ r = S \to 𝒫 r = 𝒫 S$
5	4	ineq1d	$⊢ r = S \to 𝒫 r \cap Fin = 𝒫 S \cap Fin$
6	5	rexeqdv	$⊢ r = S \to (\exists s \in (𝒫 r \cap Fin) X = ⋃ s \leftrightarrow \exists s \in (𝒫 S \cap Fin) X = ⋃ s)$
7	3 6	imbi12d	$⊢ r = S \to ((X = ⋃ r \to \exists s \in (𝒫 r \cap Fin) X = ⋃ s) \leftrightarrow (X = ⋃ S \to \exists s \in (𝒫 S \cap Fin) X = ⋃ s))$
8	1	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall r \in 𝒫 J (X = ⋃ r \to \exists s \in (𝒫 r \cap Fin) X = ⋃ s))$
9	8	simprbi	$⊢ J \in Comp \to \forall r \in 𝒫 J (X = ⋃ r \to \exists s \in (𝒫 r \cap Fin) X = ⋃ s)$
10	9	adantr	$⊢ (J \in Comp \land S \subseteq J) \to \forall r \in 𝒫 J (X = ⋃ r \to \exists s \in (𝒫 r \cap Fin) X = ⋃ s)$
11		ssexg	$⊢ (S \subseteq J \land J \in Comp) \to S \in V$
12	11	ancoms	$⊢ (J \in Comp \land S \subseteq J) \to S \in V$
13		simpr	$⊢ (J \in Comp \land S \subseteq J) \to S \subseteq J$
14	12 13	elpwd	$⊢ (J \in Comp \land S \subseteq J) \to S \in 𝒫 J$
15	7 10 14	rspcdva	$⊢ (J \in Comp \land S \subseteq J) \to (X = ⋃ S \to \exists s \in (𝒫 S \cap Fin) X = ⋃ s)$
16	15	3impia	$⊢ (J \in Comp \land S \subseteq J \land X = ⋃ S) \to \exists s \in (𝒫 S \cap Fin) X = ⋃ s$

Metamath Proof Explorer