This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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