Metamath Proof Explorer

Theorem qtopkgen

Description: A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypothesis qtopcmp.1 
|- X = U. J
Assertion qtopkgen 
|- ( ( J e. ran kGen /\ F Fn X ) -> ( J qTop F ) e. ran kGen )

Proof

Step Hyp Ref Expression
1 qtopcmp.1 
 |-  X = U. J
2 kgentop 
 |-  ( J e. ran kGen -> J e. Top )
3 1 qtoptop 
 |-  ( ( J e. Top /\ F Fn X ) -> ( J qTop F ) e. Top )
4 2 3 sylan 
 |-  ( ( J e. ran kGen /\ F Fn X ) -> ( J qTop F ) e. Top )
5 elssuni 
 |-  ( x e. ( kGen ` ( J qTop F ) ) -> x C_ U. ( kGen ` ( J qTop F ) ) )
6 5 adantl 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> x C_ U. ( kGen ` ( J qTop F ) ) )
7 4 adantr 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> ( J qTop F ) e. Top )
8 eqid 
 |-  U. ( J qTop F ) = U. ( J qTop F )
9 8 kgenuni 
 |-  ( ( J qTop F ) e. Top -> U. ( J qTop F ) = U. ( kGen ` ( J qTop F ) ) )
10 7 9 syl 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> U. ( J qTop F ) = U. ( kGen ` ( J qTop F ) ) )
11 6 10 sseqtrrd 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> x C_ U. ( J qTop F ) )
12 simpll 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> J e. ran kGen )
13 12 2 syl 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> J e. Top )
14 simplr 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> F Fn X )
15 dffn4 
 |-  ( F Fn X <-> F : X -onto-> ran F )
16 14 15 sylib 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> F : X -onto-> ran F )
17 1 qtopuni 
 |-  ( ( J e. Top /\ F : X -onto-> ran F ) -> ran F = U. ( J qTop F ) )
18 13 16 17 syl2anc 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> ran F = U. ( J qTop F ) )
19 11 18 sseqtrrd 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> x C_ ran F )
20 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
21 13 20 sylib 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> J e. ( TopOn ` X ) )
22 qtopid 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
23 21 14 22 syl2anc 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> F e. ( J Cn ( J qTop F ) ) )
24 kgencn3 
 |-  ( ( J e. ran kGen /\ ( J qTop F ) e. Top ) -> ( J Cn ( J qTop F ) ) = ( J Cn ( kGen ` ( J qTop F ) ) ) )
25 12 7 24 syl2anc 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> ( J Cn ( J qTop F ) ) = ( J Cn ( kGen ` ( J qTop F ) ) ) )
26 23 25 eleqtrd 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> F e. ( J Cn ( kGen ` ( J qTop F ) ) ) )
27 cnima 
 |-  ( ( F e. ( J Cn ( kGen ` ( J qTop F ) ) ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> ( `' F " x ) e. J )
28 26 27 sylancom 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> ( `' F " x ) e. J )
29 1 elqtop2 
 |-  ( ( J e. ran kGen /\ F : X -onto-> ran F ) -> ( x e. ( J qTop F ) <-> ( x C_ ran F /\ ( `' F " x ) e. J ) ) )
30 12 16 29 syl2anc 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> ( x e. ( J qTop F ) <-> ( x C_ ran F /\ ( `' F " x ) e. J ) ) )
31 19 28 30 mpbir2and 
 |-  ( ( ( J e. ran kGen /\ F Fn X ) /\ x e. ( kGen ` ( J qTop F ) ) ) -> x e. ( J qTop F ) )
32 31 ex 
 |-  ( ( J e. ran kGen /\ F Fn X ) -> ( x e. ( kGen ` ( J qTop F ) ) -> x e. ( J qTop F ) ) )
33 32 ssrdv 
 |-  ( ( J e. ran kGen /\ F Fn X ) -> ( kGen ` ( J qTop F ) ) C_ ( J qTop F ) )
34 iskgen2 
 |-  ( ( J qTop F ) e. ran kGen <-> ( ( J qTop F ) e. Top /\ ( kGen ` ( J qTop F ) ) C_ ( J qTop F ) ) )
35 4 33 34 sylanbrc 
 |-  ( ( J e. ran kGen /\ F Fn X ) -> ( J qTop F ) e. ran kGen )