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 )
3 2 3ad2ant1 
 |-  ( ( 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 )