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
`|- X = U. K`
Assertion sscmp
`|- ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) -> J e. Comp )`

Proof

Step Hyp Ref Expression
1 sscmp.1
` |-  X = U. K`
2 topontop
` |-  ( J e. ( TopOn ` X ) -> J e. Top )`
` |-  ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) -> J e. Top )`
4 elpwi
` |-  ( x e. ~P J -> x C_ J )`
5 simpl2
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> K e. Comp )`
6 simprl
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> x C_ J )`
7 simpl3
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> J C_ K )`
8 6 7 sstrd
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> x C_ K )`
9 simpl1
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> J e. ( TopOn ` X ) )`
10 toponuni
` |-  ( J e. ( TopOn ` X ) -> X = U. J )`
11 9 10 syl
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> X = U. J )`
12 simprr
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> U. J = U. x )`
13 11 12 eqtrd
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> X = U. x )`
14 1 cmpcov
` |-  ( ( K e. Comp /\ x C_ K /\ X = U. x ) -> E. y e. ( ~P x i^i Fin ) X = U. y )`
15 5 8 13 14 syl3anc
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )`
16 11 eqeq1d
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> ( X = U. y <-> U. J = U. y ) )`
17 16 rexbidv
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> ( E. y e. ( ~P x i^i Fin ) X = U. y <-> E. y e. ( ~P x i^i Fin ) U. J = U. y ) )`
18 15 17 mpbid
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ ( x C_ J /\ U. J = U. x ) ) -> E. y e. ( ~P x i^i Fin ) U. J = U. y )`
19 18 expr
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ x C_ J ) -> ( U. J = U. x -> E. y e. ( ~P x i^i Fin ) U. J = U. y ) )`
20 4 19 sylan2
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) /\ x e. ~P J ) -> ( U. J = U. x -> E. y e. ( ~P x i^i Fin ) U. J = U. y ) )`
21 20 ralrimiva
` |-  ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) -> A. x e. ~P J ( U. J = U. x -> E. y e. ( ~P x i^i Fin ) U. J = U. y ) )`
22 eqid
` |-  U. J = U. J`
23 22 iscmp
` |-  ( J e. Comp <-> ( J e. Top /\ A. x e. ~P J ( U. J = U. x -> E. y e. ( ~P x i^i Fin ) U. J = U. y ) ) )`
24 3 21 23 sylanbrc
` |-  ( ( J e. ( TopOn ` X ) /\ K e. Comp /\ J C_ K ) -> J e. Comp )`