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βˆˆπ’«β‹ƒjj↾𝑑k∈Compβ†’x∩k∈j↾𝑑k∈V
4 3 a1i ⊒⊀∧j∈Topβ†’xβˆˆπ’«β‹ƒj|βˆ€kβˆˆπ’«β‹ƒjj↾𝑑k∈Compβ†’x∩k∈j↾𝑑k∈V
5 df-kgen βŠ’π‘˜Gen=j∈Top⟼xβˆˆπ’«β‹ƒj|βˆ€kβˆˆπ’«β‹ƒjj↾𝑑k∈Compβ†’x∩k∈j↾𝑑k
6 5 a1i βŠ’βŠ€β†’π‘˜Gen=j∈Top⟼xβˆˆπ’«β‹ƒj|βˆ€kβˆˆπ’«β‹ƒjj↾𝑑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