Metamath Proof Explorer


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 ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )