Theorem isreg

Description: The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T_3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	isreg	⊢ ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑗 = 𝐽 → ( cls ‘ 𝑗 ) = ( cls ‘ 𝐽 ) )
2	1	fveq1d	⊢ ( 𝑗 = 𝐽 → ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) )
3	2	sseq1d	⊢ ( 𝑗 = 𝐽 → ( ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
4	3	anbi2d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
5	4	rexeqbi1dv	⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
6	5	ralbidv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
7	6	raleqbi1dv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
8		df-reg	⊢ Reg = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }
9	7 8	elrab2	⊢ ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )