Metamath Proof Explorer

Theorem nrmr0reg

Description: A normal R_0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion nrmr0reg ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → 𝐽 ∈ Reg )

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
2 1 adantr ⊢ ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → 𝐽 ∈ Top )
3 simpll ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Nrm )
4 simprl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ 𝐽 )
5 2 adantr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Top )
6 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
7 5 6 sylib ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
8 simplr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( KQ ‘ 𝐽 ) ∈ Fre )
9 simprr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑥 )
10 elunii ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐽 ) → 𝑦 ∈ ∪ 𝐽 )
11 9 4 10 syl2anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ∪ 𝐽 )
12 eqid ⊢ ( 𝑧 ∈ ∪ 𝐽 ↦ { 𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤 } ) = ( 𝑧 ∈ ∪ 𝐽 ↦ { 𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤 } )
13 12 r0cld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( KQ ‘ 𝐽 ) ∈ Fre ∧ 𝑦 ∈ ∪ 𝐽 ) → { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ∈ ( Clsd ‘ 𝐽 ) )
14 7 8 11 13 syl3anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ∈ ( Clsd ‘ 𝐽 ) )
15 simp1rr ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ) → 𝑦 ∈ 𝑥 )
16 4 adantr ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ 𝑎 ∈ ∪ 𝐽 ) → 𝑥 ∈ 𝐽 )
17 elequ2 ⊢ ( 𝑏 = 𝑥 → ( 𝑎 ∈ 𝑏 ↔ 𝑎 ∈ 𝑥 ) )
18 elequ2 ⊢ ( 𝑏 = 𝑥 → ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑥 ) )
19 17 18 bibi12d ⊢ ( 𝑏 = 𝑥 → ( ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ↔ ( 𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) ) )
20 19 rspcv ⊢ ( 𝑥 ∈ 𝐽 → ( ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) → ( 𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) ) )
21 16 20 syl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ 𝑎 ∈ ∪ 𝐽 ) → ( ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) → ( 𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) ) )
22 21 3impia ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ) → ( 𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
23 15 22 mpbird ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ) → 𝑎 ∈ 𝑥 )
24 23 rabssdv ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑥 )
25 nrmsep3 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝑥 ∈ 𝐽 ∧ { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ∈ ( Clsd ‘ 𝐽 ) ∧ { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐽 ( { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
26 3 4 14 24 25 syl13anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐽 ( { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
27 elequ1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) )
28 27 bibi1d ⊢ ( 𝑎 = 𝑦 → ( ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ↔ ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ) )
29 28 ralbidv ⊢ ( 𝑎 = 𝑦 → ( ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐽 ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) ) )
30 biidd ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) )
31 30 ralrimivw ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∀ 𝑏 ∈ 𝐽 ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) )
32 29 11 31 elrabd ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } )
33 ssel ⊢ ( { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑧 → ( 𝑦 ∈ { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } → 𝑦 ∈ 𝑧 ) )
34 32 33 syl5com ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑧 → 𝑦 ∈ 𝑧 ) )
35 34 anim1d ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) → ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
36 35 reximdv ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∃ 𝑧 ∈ 𝐽 ( { 𝑎 ∈ ∪ 𝐽 ∣ ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏 ) } ⊆ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
37 26 36 mpd ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
38 37 ralrimivva ⊢ ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
39 isreg ⊢ ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐽 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
40 2 38 39 sylanbrc ⊢ ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → 𝐽 ∈ Reg )