Theorem ist1

Description: The predicate "is a T_1 space". (Contributed by FL, 18-Jun-2007)

	Ref	Expression
Hypothesis	ist0.1	$$⊢X=\bigcup J$$
Assertion	ist1	$$⊢J\in \mathrm{Fre}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall a\in X\left\{a\right\}\in \mathrm{Clsd}\left(J\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ist0.1	$$⊢X=\bigcup J$$
2		unieq	$$⊢x=J\to \bigcup x=\bigcup J$$
3	2 1	eqtr4di	$$⊢x=J\to \bigcup x=X$$
4		fveq2	$$⊢x=J\to \mathrm{Clsd}\left(x\right)=\mathrm{Clsd}\left(J\right)$$
5	4	eleq2d	$$⊢x=J\to \left(\left\{a\right\}\in \mathrm{Clsd}\left(x\right)\leftrightarrow \left\{a\right\}\in \mathrm{Clsd}\left(J\right)\right)$$
6	3 5	raleqbidv	$$⊢x=J\to \left(\forall a\in \bigcup x\left\{a\right\}\in \mathrm{Clsd}\left(x\right)\leftrightarrow \forall a\in X\left\{a\right\}\in \mathrm{Clsd}\left(J\right)\right)$$
7		df-t1	$$⊢\mathrm{Fre}=\left\{x\in \mathrm{Top}|\forall a\in \bigcup x\left\{a\right\}\in \mathrm{Clsd}\left(x\right)\right\}$$
8	6 7	elrab2	$$⊢J\in \mathrm{Fre}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall a\in X\left\{a\right\}\in \mathrm{Clsd}\left(J\right)\right)$$