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 ⊢ 𝑋 = ∪ 𝐽
Assertion qtopkgen ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ ran 𝑘Gen )

Proof

Step Hyp Ref Expression
1 qtopcmp.1 ⊢ 𝑋 = ∪ 𝐽
2 kgentop ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )
3 1 qtoptop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
4 2 3 sylan ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
5 elssuni ⊢ ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) → 𝑥 ⊆ ∪ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) )
6 5 adantl ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝑥 ⊆ ∪ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) )
7 4 adantr ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
8 eqid ⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
9 8 kgenuni ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ Top → ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) )
10 7 9 syl ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) )
11 6 10 sseqtrrd ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝑥 ⊆ ∪ ( 𝐽 qTop 𝐹 ) )
12 simpll ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐽 ∈ ran 𝑘Gen )
13 12 2 syl ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐽 ∈ Top )
14 simplr ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐹 Fn 𝑋 )
15 dffn4 ⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
16 14 15 sylib ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
17 1 qtopuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ran 𝐹 = ∪ ( 𝐽 qTop 𝐹 ) )
18 13 16 17 syl2anc ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ran 𝐹 = ∪ ( 𝐽 qTop 𝐹 ) )
19 11 18 sseqtrrd ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝑥 ⊆ ran 𝐹 )
20 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
21 13 20 sylib ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
22 qtopid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
23 21 14 22 syl2anc ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
24 kgencn3 ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ ( 𝐽 qTop 𝐹 ) ∈ Top ) → ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) = ( 𝐽 Cn ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) )
25 12 7 24 syl2anc ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) = ( 𝐽 Cn ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) )
26 23 25 eleqtrd ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) )
27 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
28 26 27 sylancom ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
29 1 elqtop2 ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
30 12 16 29 syl2anc ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
31 19 28 30 mpbir2and ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ) → 𝑥 ∈ ( 𝐽 qTop 𝐹 ) )
32 31 ex ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) → 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ) )
33 32 ssrdv ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) → ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ⊆ ( 𝐽 qTop 𝐹 ) )
34 iskgen2 ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ ran 𝑘Gen ↔ ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ ( 𝑘Gen ‘ ( 𝐽 qTop 𝐹 ) ) ⊆ ( 𝐽 qTop 𝐹 ) ) )
35 4 33 34 sylanbrc ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ ran 𝑘Gen )