Theorem fncld

Description: The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fncld	⊢ Clsd Fn Top

Proof

Step	Hyp	Ref	Expression
1		vuniex	⊢ ∪ 𝑗 ∈ V
2	1	pwex	⊢ 𝒫 ∪ 𝑗 ∈ V
3	2	rabex	⊢ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } ∈ V
4		df-cld	⊢ Clsd = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } )
5	3 4	fnmpti	⊢ Clsd Fn Top