sscmp

Description: A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Hypothesis	sscmp.1	$⊢ X = ⋃ K$
	Assertion	sscmp	$⊢ (J \in TopOn (X) \land K \in Comp \land J \subseteq K) \to J \in Comp$

Proof

Step	Hyp	Ref	Expression
1		sscmp.1	$⊢ X = ⋃ K$
2		topontop	$⊢ J \in TopOn (X) \to J \in Top$
3	2	3ad2ant1	$⊢ (J \in TopOn (X) \land K \in Comp \land J \subseteq K) \to J \in Top$
4		elpwi	$⊢ x \in 𝒫 J \to x \subseteq J$
5		simpl2	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to K \in Comp$
6		simprl	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to x \subseteq J$
7		simpl3	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to J \subseteq K$
8	6 7	sstrd	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to x \subseteq K$
9		simpl1	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to J \in TopOn (X)$
10		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
11	9 10	syl	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to X = ⋃ J$
12		simprr	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to ⋃ J = ⋃ x$
13	11 12	eqtrd	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to X = ⋃ x$
14	1	cmpcov	$⊢ (K \in Comp \land x \subseteq K \land X = ⋃ x) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
15	5 8 13 14	syl3anc	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
16	11	eqeq1d	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to (X = ⋃ y \leftrightarrow ⋃ J = ⋃ y)$
17	16	rexbidv	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to (\exists y \in (𝒫 x \cap Fin) X = ⋃ y \leftrightarrow \exists y \in (𝒫 x \cap Fin) ⋃ J = ⋃ y)$
18	15 17	mpbid	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land (x \subseteq J \land ⋃ J = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) ⋃ J = ⋃ y$
19	18	expr	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land x \subseteq J) \to (⋃ J = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ J = ⋃ y)$
20	4 19	sylan2	$⊢ ((J \in TopOn (X) \land K \in Comp \land J \subseteq K) \land x \in 𝒫 J) \to (⋃ J = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ J = ⋃ y)$
21	20	ralrimiva	$⊢ (J \in TopOn (X) \land K \in Comp \land J \subseteq K) \to \forall x \in 𝒫 J (⋃ J = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ J = ⋃ y)$
22		eqid	$⊢ ⋃ J = ⋃ J$
23	22	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall x \in 𝒫 J (⋃ J = ⋃ x \to \exists y \in (𝒫 x \cap Fin) ⋃ J = ⋃ y))$
24	3 21 23	sylanbrc	$⊢ (J \in TopOn (X) \land K \in Comp \land J \subseteq K) \to J \in Comp$

Metamath Proof Explorer

Theorem sscmp

Proof