Theorem kgenf

Description: The compact generator is a function on topologies. (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Assertion	kgenf	⊢ 𝑘Gen : Top ⟶ Top

Proof

Step	Hyp	Ref	Expression
1		vuniex	⊢ ∪ 𝑗 ∈ V
2	1	pwex	⊢ 𝒫 ∪ 𝑗 ∈ V
3	2	rabex	⊢ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } ∈ V
4	3	a1i	⊢ ( ( ⊤ ∧ 𝑗 ∈ Top ) → { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } ∈ V )
5		df-kgen	⊢ 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } )
6	5	a1i	⊢ ( ⊤ → 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } ) )
7		kgenftop	⊢ ( 𝑥 ∈ Top → ( 𝑘Gen ‘ 𝑥 ) ∈ Top )
8	7	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ Top ) → ( 𝑘Gen ‘ 𝑥 ) ∈ Top )
9	4 6 8	fmpt2d	⊢ ( ⊤ → 𝑘Gen : Top ⟶ Top )
10	9	mptru	⊢ 𝑘Gen : Top ⟶ Top