Metamath Proof Explorer

Theorem kgencmp

Description: The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgencmp 
|- ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) = ( ( kGen ` J ) |`t K ) )

Proof

Step Hyp Ref Expression
1 kgenftop 
 |-  ( J e. Top -> ( kGen ` J ) e. Top )
2 1 adantr 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( kGen ` J ) e. Top )
3 kgenss 
 |-  ( J e. Top -> J C_ ( kGen ` J ) )
4 3 adantr 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> J C_ ( kGen ` J ) )
5 ssrest 
 |-  ( ( ( kGen ` J ) e. Top /\ J C_ ( kGen ` J ) ) -> ( J |`t K ) C_ ( ( kGen ` J ) |`t K ) )
6 2 4 5 syl2anc 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) C_ ( ( kGen ` J ) |`t K ) )
7 cmptop 
 |-  ( ( J |`t K ) e. Comp -> ( J |`t K ) e. Top )
8 7 adantl 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) e. Top )
9 restrcl 
 |-  ( ( J |`t K ) e. Top -> ( J e. _V /\ K e. _V ) )
10 9 simprd 
 |-  ( ( J |`t K ) e. Top -> K e. _V )
11 8 10 syl 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> K e. _V )
12 restval 
 |-  ( ( ( kGen ` J ) e. Top /\ K e. _V ) -> ( ( kGen ` J ) |`t K ) = ran ( x e. ( kGen ` J ) |-> ( x i^i K ) ) )
13 2 11 12 syl2anc 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( ( kGen ` J ) |`t K ) = ran ( x e. ( kGen ` J ) |-> ( x i^i K ) ) )
14 simpr 
 |-  ( ( ( J e. Top /\ ( J |`t K ) e. Comp ) /\ x e. ( kGen ` J ) ) -> x e. ( kGen ` J ) )
15 simplr 
 |-  ( ( ( J e. Top /\ ( J |`t K ) e. Comp ) /\ x e. ( kGen ` J ) ) -> ( J |`t K ) e. Comp )
16 kgeni 
 |-  ( ( x e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( x i^i K ) e. ( J |`t K ) )
17 14 15 16 syl2anc 
 |-  ( ( ( J e. Top /\ ( J |`t K ) e. Comp ) /\ x e. ( kGen ` J ) ) -> ( x i^i K ) e. ( J |`t K ) )
18 17 fmpttd 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( x e. ( kGen ` J ) |-> ( x i^i K ) ) : ( kGen ` J ) --> ( J |`t K ) )
19 18 frnd 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ran ( x e. ( kGen ` J ) |-> ( x i^i K ) ) C_ ( J |`t K ) )
20 13 19 eqsstrd 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( ( kGen ` J ) |`t K ) C_ ( J |`t K ) )
21 6 20 eqssd 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) = ( ( kGen ` J ) |`t K ) )