Theorem ist1

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

	Ref	Expression
Hypothesis	ist0.1	⊢ 𝑋 = ∪ 𝐽
Assertion	ist1	⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎 ∈ 𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	⊢ 𝑋 = ∪ 𝐽
2		unieq	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽 )
3	2 1	eqtr4di	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = 𝑋 )
4		fveq2	⊢ ( 𝑥 = 𝐽 → ( Clsd ‘ 𝑥 ) = ( Clsd ‘ 𝐽 ) )
5	4	eleq2d	⊢ ( 𝑥 = 𝐽 → ( { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) ↔ { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )
6	3 5	raleqbidv	⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) ↔ ∀ 𝑎 ∈ 𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )
7		df-t1	⊢ Fre = { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }
8	6 7	elrab2	⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎 ∈ 𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )