Metamath Proof Explorer

Theorem kgenidm

Description: The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenidm 
|- ( J e. ran kGen -> ( kGen ` J ) = J )

Proof

Step Hyp Ref Expression
1 kgenf 
 |-  kGen : Top --> Top
2 ffn 
 |-  ( kGen : Top --> Top -> kGen Fn Top )
3 fvelrnb 
 |-  ( kGen Fn Top -> ( J e. ran kGen <-> E. j e. Top ( kGen ` j ) = J ) )
4 1 2 3 mp2b 
 |-  ( J e. ran kGen <-> E. j e. Top ( kGen ` j ) = J )
5 toptopon2 
 |-  ( j e. Top <-> j e. ( TopOn ` U. j ) )
6 kgentopon 
 |-  ( j e. ( TopOn ` U. j ) -> ( kGen ` j ) e. ( TopOn ` U. j ) )
7 5 6 sylbi 
 |-  ( j e. Top -> ( kGen ` j ) e. ( TopOn ` U. j ) )
8 kgentopon 
 |-  ( ( kGen ` j ) e. ( TopOn ` U. j ) -> ( kGen ` ( kGen ` j ) ) e. ( TopOn ` U. j ) )
9 7 8 syl 
 |-  ( j e. Top -> ( kGen ` ( kGen ` j ) ) e. ( TopOn ` U. j ) )
10 toponss 
 |-  ( ( ( kGen ` ( kGen ` j ) ) e. ( TopOn ` U. j ) /\ x e. ( kGen ` ( kGen ` j ) ) ) -> x C_ U. j )
11 9 10 sylan 
 |-  ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) -> x C_ U. j )
12 simplr 
 |-  ( ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) /\ ( k e. ~P U. j /\ ( j |`t k ) e. Comp ) ) -> x e. ( kGen ` ( kGen ` j ) ) )
13 kgencmp2 
 |-  ( j e. Top -> ( ( j |`t k ) e. Comp <-> ( ( kGen ` j ) |`t k ) e. Comp ) )
14 13 biimpa 
 |-  ( ( j e. Top /\ ( j |`t k ) e. Comp ) -> ( ( kGen ` j ) |`t k ) e. Comp )
15 14 ad2ant2rl 
 |-  ( ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) /\ ( k e. ~P U. j /\ ( j |`t k ) e. Comp ) ) -> ( ( kGen ` j ) |`t k ) e. Comp )
16 kgeni 
 |-  ( ( x e. ( kGen ` ( kGen ` j ) ) /\ ( ( kGen ` j ) |`t k ) e. Comp ) -> ( x i^i k ) e. ( ( kGen ` j ) |`t k ) )
17 12 15 16 syl2anc 
 |-  ( ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) /\ ( k e. ~P U. j /\ ( j |`t k ) e. Comp ) ) -> ( x i^i k ) e. ( ( kGen ` j ) |`t k ) )
18 kgencmp 
 |-  ( ( j e. Top /\ ( j |`t k ) e. Comp ) -> ( j |`t k ) = ( ( kGen ` j ) |`t k ) )
19 18 ad2ant2rl 
 |-  ( ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) /\ ( k e. ~P U. j /\ ( j |`t k ) e. Comp ) ) -> ( j |`t k ) = ( ( kGen ` j ) |`t k ) )
20 17 19 eleqtrrd 
 |-  ( ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) /\ ( k e. ~P U. j /\ ( j |`t k ) e. Comp ) ) -> ( x i^i k ) e. ( j |`t k ) )
21 20 expr 
 |-  ( ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) /\ k e. ~P U. j ) -> ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) )
22 21 ralrimiva 
 |-  ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) -> A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) )
23 5 birani 
 |-  ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) -> j e. ( TopOn ` U. j ) )
24 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 ) ) ) ) )
25 23 24 syl 
 |-  ( ( j e. Top /\ x e. ( kGen ` ( kGen ` 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 ) ) ) ) )
26 11 22 25 mpbir2and 
 |-  ( ( j e. Top /\ x e. ( kGen ` ( kGen ` j ) ) ) -> x e. ( kGen ` j ) )
27 26 ex 
 |-  ( j e. Top -> ( x e. ( kGen ` ( kGen ` j ) ) -> x e. ( kGen ` j ) ) )
28 27 ssrdv 
 |-  ( j e. Top -> ( kGen ` ( kGen ` j ) ) C_ ( kGen ` j ) )
29 fveq2 
 |-  ( ( kGen ` j ) = J -> ( kGen ` ( kGen ` j ) ) = ( kGen ` J ) )
30 id 
 |-  ( ( kGen ` j ) = J -> ( kGen ` j ) = J )
31 29 30 sseq12d 
 |-  ( ( kGen ` j ) = J -> ( ( kGen ` ( kGen ` j ) ) C_ ( kGen ` j ) <-> ( kGen ` J ) C_ J ) )
32 28 31 syl5ibcom 
 |-  ( j e. Top -> ( ( kGen ` j ) = J -> ( kGen ` J ) C_ J ) )
33 32 rexlimiv 
 |-  ( E. j e. Top ( kGen ` j ) = J -> ( kGen ` J ) C_ J )
34 4 33 sylbi 
 |-  ( J e. ran kGen -> ( kGen ` J ) C_ J )
35 kgentop 
 |-  ( J e. ran kGen -> J e. Top )
36 kgenss 
 |-  ( J e. Top -> J C_ ( kGen ` J ) )
37 35 36 syl 
 |-  ( J e. ran kGen -> J C_ ( kGen ` J ) )
38 34 37 eqssd 
 |-  ( J e. ran kGen -> ( kGen ` J ) = J )