Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ∪ 𝐾
Assertion sscmp ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ Comp )

Proof

Step Hyp Ref Expression
1 sscmp.1 ⊢ 𝑋 = ∪ 𝐾
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ Top )
4 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐽 → 𝑥 ⊆ 𝐽 )
5 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝐾 ∈ Comp )
6 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝑥 ⊆ 𝐽 )
7 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝐽 ⊆ 𝐾 )
8 6 7 sstrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝑥 ⊆ 𝐾 )
9 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
11 9 10 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝑋 = ∪ 𝐽 )
12 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → ∪ 𝐽 = ∪ 𝑥 )
13 11 12 eqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → 𝑋 = ∪ 𝑥 )
14 1 cmpcov ⊢ ( ( 𝐾 ∈ Comp ∧ 𝑥 ⊆ 𝐾 ∧ 𝑋 = ∪ 𝑥 ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
15 5 8 13 14 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
16 11 eqeq1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → ( 𝑋 = ∪ 𝑦 ↔ ∪ 𝐽 = ∪ 𝑦 ) )
17 16 rexbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → ( ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 ↔ ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∪ 𝐽 = ∪ 𝑦 ) )
18 15 17 mpbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∪ 𝐽 = ∪ 𝑦 )
19 18 expr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ⊆ 𝐽 ) → ( ∪ 𝐽 = ∪ 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∪ 𝐽 = ∪ 𝑦 ) )
20 4 19 sylan2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ 𝒫 𝐽 ) → ( ∪ 𝐽 = ∪ 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∪ 𝐽 = ∪ 𝑦 ) )
21 20 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) → ∀ 𝑥 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∪ 𝐽 = ∪ 𝑦 ) )
22 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
23 22 iscmp ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∪ 𝐽 = ∪ 𝑦 ) ) )
24 3 21 23 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ Comp )