Metamath Proof Explorer

Theorem kgenss

Description: The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenss 
|- ( J e. Top -> J C_ ( kGen ` J ) )

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( x e. J -> x C_ U. J )
2 1 a1i 
 |-  ( J e. Top -> ( x e. J -> x C_ U. J ) )
3 elrestr 
 |-  ( ( J e. Top /\ k e. ~P U. J /\ x e. J ) -> ( x i^i k ) e. ( J |`t k ) )
4 3 3expa 
 |-  ( ( ( J e. Top /\ k e. ~P U. J ) /\ x e. J ) -> ( x i^i k ) e. ( J |`t k ) )
5 4 an32s 
 |-  ( ( ( J e. Top /\ x e. J ) /\ k e. ~P U. J ) -> ( x i^i k ) e. ( J |`t k ) )
6 5 a1d 
 |-  ( ( ( J e. Top /\ x e. J ) /\ k e. ~P U. J ) -> ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) )
7 6 ralrimiva 
 |-  ( ( J e. Top /\ x e. J ) -> A. k e. ~P U. J ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) )
8 7 ex 
 |-  ( J e. Top -> ( x e. J -> A. k e. ~P U. J ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) )
9 2 8 jcad 
 |-  ( J e. Top -> ( x e. J -> ( x C_ U. J /\ A. k e. ~P U. J ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )
10 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
11 elkgen 
 |-  ( J e. ( TopOn ` U. J ) -> ( x e. ( kGen ` J ) <-> ( x C_ U. J /\ A. k e. ~P U. J ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )
12 10 11 sylbi 
 |-  ( J e. Top -> ( x e. ( kGen ` J ) <-> ( x C_ U. J /\ A. k e. ~P U. J ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )
13 9 12 sylibrd 
 |-  ( J e. Top -> ( x e. J -> x e. ( kGen ` J ) ) )
14 13 ssrdv 
 |-  ( J e. Top -> J C_ ( kGen ` J ) )