# 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 )