Metamath Proof Explorer

Theorem kgentopon

Description: The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion kgentopon 
|- ( J e. ( TopOn ` X ) -> ( kGen ` J ) e. ( TopOn ` X ) )

Proof

Step Hyp Ref Expression
1 uniss 
 |-  ( x C_ ( kGen ` J ) -> U. x C_ U. ( kGen ` J ) )
2 kgenval 
 |-  ( J e. ( TopOn ` X ) -> ( kGen ` J ) = { x e. ~P X | A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) } )
3 ssrab2 
 |-  { x e. ~P X | A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) } C_ ~P X
4 2 3 eqsstrdi 
 |-  ( J e. ( TopOn ` X ) -> ( kGen ` J ) C_ ~P X )
5 sspwuni 
 |-  ( ( kGen ` J ) C_ ~P X <-> U. ( kGen ` J ) C_ X )
6 4 5 sylib 
 |-  ( J e. ( TopOn ` X ) -> U. ( kGen ` J ) C_ X )
7 1 6 sylan9ssr 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) -> U. x C_ X )
8 iunin2 
 |-  U_ y e. x ( k i^i y ) = ( k i^i U_ y e. x y )
9 uniiun 
 |-  U. x = U_ y e. x y
10 9 ineq2i 
 |-  ( k i^i U. x ) = ( k i^i U_ y e. x y )
11 incom 
 |-  ( k i^i U. x ) = ( U. x i^i k )
12 8 10 11 3eqtr2i 
 |-  U_ y e. x ( k i^i y ) = ( U. x i^i k )
13 cmptop 
 |-  ( ( J |`t k ) e. Comp -> ( J |`t k ) e. Top )
14 13 ad2antll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( J |`t k ) e. Top )
15 incom 
 |-  ( y i^i k ) = ( k i^i y )
16 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> x C_ ( kGen ` J ) )
17 16 sselda 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) /\ y e. x ) -> y e. ( kGen ` J ) )
18 simplrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) /\ y e. x ) -> ( J |`t k ) e. Comp )
19 kgeni 
 |-  ( ( y e. ( kGen ` J ) /\ ( J |`t k ) e. Comp ) -> ( y i^i k ) e. ( J |`t k ) )
20 17 18 19 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) /\ y e. x ) -> ( y i^i k ) e. ( J |`t k ) )
21 15 20 eqeltrrid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) /\ y e. x ) -> ( k i^i y ) e. ( J |`t k ) )
22 21 ralrimiva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> A. y e. x ( k i^i y ) e. ( J |`t k ) )
23 iunopn 
 |-  ( ( ( J |`t k ) e. Top /\ A. y e. x ( k i^i y ) e. ( J |`t k ) ) -> U_ y e. x ( k i^i y ) e. ( J |`t k ) )
24 14 22 23 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> U_ y e. x ( k i^i y ) e. ( J |`t k ) )
25 12 24 eqeltrrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( U. x i^i k ) e. ( J |`t k ) )
26 25 expr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) /\ k e. ~P X ) -> ( ( J |`t k ) e. Comp -> ( U. x i^i k ) e. ( J |`t k ) ) )
27 26 ralrimiva 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) -> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( U. x i^i k ) e. ( J |`t k ) ) )
28 elkgen 
 |-  ( J e. ( TopOn ` X ) -> ( U. x e. ( kGen ` J ) <-> ( U. x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( U. x i^i k ) e. ( J |`t k ) ) ) ) )
29 28 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) -> ( U. x e. ( kGen ` J ) <-> ( U. x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( U. x i^i k ) e. ( J |`t k ) ) ) ) )
30 7 27 29 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ ( kGen ` J ) ) -> U. x e. ( kGen ` J ) )
31 30 ex 
 |-  ( J e. ( TopOn ` X ) -> ( x C_ ( kGen ` J ) -> U. x e. ( kGen ` J ) ) )
32 31 alrimiv 
 |-  ( J e. ( TopOn ` X ) -> A. x ( x C_ ( kGen ` J ) -> U. x e. ( kGen ` J ) ) )
33 inss1 
 |-  ( x i^i y ) C_ x
34 elssuni 
 |-  ( x e. ( kGen ` J ) -> x C_ U. ( kGen ` J ) )
35 34 ad2antrl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> x C_ U. ( kGen ` J ) )
36 ssidd 
 |-  ( J e. ( TopOn ` X ) -> X C_ X )
37 elpwi 
 |-  ( k e. ~P X -> k C_ X )
38 37 ad2antrl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> k C_ X )
39 sseqin2 
 |-  ( k C_ X <-> ( X i^i k ) = k )
40 38 39 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( X i^i k ) = k )
41 37 adantr 
 |-  ( ( k e. ~P X /\ ( J |`t k ) e. Comp ) -> k C_ X )
42 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ k C_ X ) -> ( J |`t k ) e. ( TopOn ` k ) )
43 41 42 sylan2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( J |`t k ) e. ( TopOn ` k ) )
44 toponmax 
 |-  ( ( J |`t k ) e. ( TopOn ` k ) -> k e. ( J |`t k ) )
45 43 44 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> k e. ( J |`t k ) )
46 40 45 eqeltrd 
 |-  ( ( J e. ( TopOn ` X ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( X i^i k ) e. ( J |`t k ) )
47 46 expr 
 |-  ( ( J e. ( TopOn ` X ) /\ k e. ~P X ) -> ( ( J |`t k ) e. Comp -> ( X i^i k ) e. ( J |`t k ) ) )
48 47 ralrimiva 
 |-  ( J e. ( TopOn ` X ) -> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( X i^i k ) e. ( J |`t k ) ) )
49 elkgen 
 |-  ( J e. ( TopOn ` X ) -> ( X e. ( kGen ` J ) <-> ( X C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( X i^i k ) e. ( J |`t k ) ) ) ) )
50 36 48 49 mpbir2and 
 |-  ( J e. ( TopOn ` X ) -> X e. ( kGen ` J ) )
51 elssuni 
 |-  ( X e. ( kGen ` J ) -> X C_ U. ( kGen ` J ) )
52 50 51 syl 
 |-  ( J e. ( TopOn ` X ) -> X C_ U. ( kGen ` J ) )
53 52 6 eqssd 
 |-  ( J e. ( TopOn ` X ) -> X = U. ( kGen ` J ) )
54 53 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> X = U. ( kGen ` J ) )
55 35 54 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> x C_ X )
56 33 55 sstrid 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> ( x i^i y ) C_ X )
57 inindir 
 |-  ( ( x i^i y ) i^i k ) = ( ( x i^i k ) i^i ( y i^i k ) )
58 13 ad2antll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( J |`t k ) e. Top )
59 simplrl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> x e. ( kGen ` J ) )
60 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( J |`t k ) e. Comp )
61 kgeni 
 |-  ( ( x e. ( kGen ` J ) /\ ( J |`t k ) e. Comp ) -> ( x i^i k ) e. ( J |`t k ) )
62 59 60 61 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( x i^i k ) e. ( J |`t k ) )
63 simplrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> y e. ( kGen ` J ) )
64 63 60 19 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( y i^i k ) e. ( J |`t k ) )
65 inopn 
 |-  ( ( ( J |`t k ) e. Top /\ ( x i^i k ) e. ( J |`t k ) /\ ( y i^i k ) e. ( J |`t k ) ) -> ( ( x i^i k ) i^i ( y i^i k ) ) e. ( J |`t k ) )
66 58 62 64 65 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( ( x i^i k ) i^i ( y i^i k ) ) e. ( J |`t k ) )
67 57 66 eqeltrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ ( k e. ~P X /\ ( J |`t k ) e. Comp ) ) -> ( ( x i^i y ) i^i k ) e. ( J |`t k ) )
68 67 expr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) /\ k e. ~P X ) -> ( ( J |`t k ) e. Comp -> ( ( x i^i y ) i^i k ) e. ( J |`t k ) ) )
69 68 ralrimiva 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( x i^i y ) i^i k ) e. ( J |`t k ) ) )
70 elkgen 
 |-  ( J e. ( TopOn ` X ) -> ( ( x i^i y ) e. ( kGen ` J ) <-> ( ( x i^i y ) C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( x i^i y ) i^i k ) e. ( J |`t k ) ) ) ) )
71 70 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> ( ( x i^i y ) e. ( kGen ` J ) <-> ( ( x i^i y ) C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( x i^i y ) i^i k ) e. ( J |`t k ) ) ) ) )
72 56 69 71 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x e. ( kGen ` J ) /\ y e. ( kGen ` J ) ) ) -> ( x i^i y ) e. ( kGen ` J ) )
73 72 ralrimivva 
 |-  ( J e. ( TopOn ` X ) -> A. x e. ( kGen ` J ) A. y e. ( kGen ` J ) ( x i^i y ) e. ( kGen ` J ) )
74 fvex 
 |-  ( kGen ` J ) e. _V
75 istopg 
 |-  ( ( kGen ` J ) e. _V -> ( ( kGen ` J ) e. Top <-> ( A. x ( x C_ ( kGen ` J ) -> U. x e. ( kGen ` J ) ) /\ A. x e. ( kGen ` J ) A. y e. ( kGen ` J ) ( x i^i y ) e. ( kGen ` J ) ) ) )
76 74 75 ax-mp 
 |-  ( ( kGen ` J ) e. Top <-> ( A. x ( x C_ ( kGen ` J ) -> U. x e. ( kGen ` J ) ) /\ A. x e. ( kGen ` J ) A. y e. ( kGen ` J ) ( x i^i y ) e. ( kGen ` J ) ) )
77 32 73 76 sylanbrc 
 |-  ( J e. ( TopOn ` X ) -> ( kGen ` J ) e. Top )
78 istopon 
 |-  ( ( kGen ` J ) e. ( TopOn ` X ) <-> ( ( kGen ` J ) e. Top /\ X = U. ( kGen ` J ) ) )
79 77 53 78 sylanbrc 
 |-  ( J e. ( TopOn ` X ) -> ( kGen ` J ) e. ( TopOn ` X ) )