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 ⊢ ⋃ j ∈ V
2 1 pwex ⊢ 𝒫 ⋃ j ∈ V
3 2 rabex ⊢ x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k ∈ V
4 3 a1i ⊢ ⊤ ∧ j ∈ Top → x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k ∈ V
5 df-kgen ⊢ 𝑘Gen = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k
6 5 a1i ⊢ ⊤ → 𝑘Gen = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k
7 kgenftop ⊢ x ∈ Top → 𝑘Gen ⁡ x ∈ Top
8 7 adantl ⊢ ⊤ ∧ x ∈ Top → 𝑘Gen ⁡ x ∈ Top
9 4 6 8 fmpt2d ⊢ ⊤ → 𝑘Gen : Top ⟶ Top
10 9 mptru ⊢ 𝑘Gen : Top ⟶ Top