Metamath Proof Explorer

Theorem kgencmp2

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

Ref Expression
Assertion kgencmp2 
|- ( J e. Top -> ( ( J |`t K ) e. Comp <-> ( ( kGen ` J ) |`t K ) e. Comp ) )

Proof

Step Hyp Ref Expression
1 kgencmp 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) = ( ( kGen ` J ) |`t K ) )
2 simpr 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) e. Comp )
3 1 2 eqeltrrd 
 |-  ( ( J e. Top /\ ( J |`t K ) e. Comp ) -> ( ( kGen ` J ) |`t K ) e. Comp )
4 cmptop 
 |-  ( ( ( kGen ` J ) |`t K ) e. Comp -> ( ( kGen ` J ) |`t K ) e. Top )
5 restrcl 
 |-  ( ( ( kGen ` J ) |`t K ) e. Top -> ( ( kGen ` J ) e. _V /\ K e. _V ) )
6 5 simprd 
 |-  ( ( ( kGen ` J ) |`t K ) e. Top -> K e. _V )
7 4 6 syl 
 |-  ( ( ( kGen ` J ) |`t K ) e. Comp -> K e. _V )
8 resttop 
 |-  ( ( J e. Top /\ K e. _V ) -> ( J |`t K ) e. Top )
9 7 8 sylan2 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( J |`t K ) e. Top )
10 toptopon2 
 |-  ( ( J |`t K ) e. Top <-> ( J |`t K ) e. ( TopOn ` U. ( J |`t K ) ) )
11 9 10 sylib 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( J |`t K ) e. ( TopOn ` U. ( J |`t K ) ) )
12 eqid 
 |-  U. J = U. J
13 12 kgenuni 
 |-  ( J e. Top -> U. J = U. ( kGen ` J ) )
14 13 adantr 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> U. J = U. ( kGen ` J ) )
15 14 ineq2d 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( K i^i U. J ) = ( K i^i U. ( kGen ` J ) ) )
16 12 restuni2 
 |-  ( ( J e. Top /\ K e. _V ) -> ( K i^i U. J ) = U. ( J |`t K ) )
17 7 16 sylan2 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( K i^i U. J ) = U. ( J |`t K ) )
18 kgenftop 
 |-  ( J e. Top -> ( kGen ` J ) e. Top )
19 eqid 
 |-  U. ( kGen ` J ) = U. ( kGen ` J )
20 19 restuni2 
 |-  ( ( ( kGen ` J ) e. Top /\ K e. _V ) -> ( K i^i U. ( kGen ` J ) ) = U. ( ( kGen ` J ) |`t K ) )
21 18 7 20 syl2an 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( K i^i U. ( kGen ` J ) ) = U. ( ( kGen ` J ) |`t K ) )
22 15 17 21 3eqtr3d 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> U. ( J |`t K ) = U. ( ( kGen ` J ) |`t K ) )
23 22 fveq2d 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( TopOn ` U. ( J |`t K ) ) = ( TopOn ` U. ( ( kGen ` J ) |`t K ) ) )
24 11 23 eleqtrd 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( J |`t K ) e. ( TopOn ` U. ( ( kGen ` J ) |`t K ) ) )
25 simpr 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( ( kGen ` J ) |`t K ) e. Comp )
26 kgenss 
 |-  ( J e. Top -> J C_ ( kGen ` J ) )
27 26 adantr 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> J C_ ( kGen ` J ) )
28 ssrest 
 |-  ( ( ( kGen ` J ) e. Top /\ J C_ ( kGen ` J ) ) -> ( J |`t K ) C_ ( ( kGen ` J ) |`t K ) )
29 18 27 28 syl2an2r 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( J |`t K ) C_ ( ( kGen ` J ) |`t K ) )
30 eqid 
 |-  U. ( ( kGen ` J ) |`t K ) = U. ( ( kGen ` J ) |`t K )
31 30 sscmp 
 |-  ( ( ( J |`t K ) e. ( TopOn ` U. ( ( kGen ` J ) |`t K ) ) /\ ( ( kGen ` J ) |`t K ) e. Comp /\ ( J |`t K ) C_ ( ( kGen ` J ) |`t K ) ) -> ( J |`t K ) e. Comp )
32 24 25 29 31 syl3anc 
 |-  ( ( J e. Top /\ ( ( kGen ` J ) |`t K ) e. Comp ) -> ( J |`t K ) e. Comp )
33 3 32 impbida 
 |-  ( J e. Top -> ( ( J |`t K ) e. Comp <-> ( ( kGen ` J ) |`t K ) e. Comp ) )