MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nrmr0reg Structured version   Visualization version   GIF version

Theorem nrmr0reg 21878
Description: A normal R0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
nrmr0reg ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Reg)

Proof of Theorem nrmr0reg
Dummy variables 𝑥 𝑦 𝑎 𝑏 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nrmtop 21466 . . 3 (𝐽 ∈ Nrm → 𝐽 ∈ Top)
21adantr 473 . 2 ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Top)
3 simpll 784 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝐽 ∈ Nrm)
4 simprl 788 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑥𝐽)
52adantr 473 . . . . . . 7 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝐽 ∈ Top)
6 eqid 2797 . . . . . . . 8 𝐽 = 𝐽
76toptopon 21047 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
85, 7sylib 210 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝐽 ∈ (TopOn‘ 𝐽))
9 simplr 786 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (KQ‘𝐽) ∈ Fre)
10 simprr 790 . . . . . . 7 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑦𝑥)
11 elunii 4631 . . . . . . 7 ((𝑦𝑥𝑥𝐽) → 𝑦 𝐽)
1210, 4, 11syl2anc 580 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑦 𝐽)
13 eqid 2797 . . . . . . 7 (𝑧 𝐽 ↦ {𝑤𝐽𝑧𝑤}) = (𝑧 𝐽 ↦ {𝑤𝐽𝑧𝑤})
1413r0cld 21867 . . . . . 6 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝑦 𝐽) → {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ∈ (Clsd‘𝐽))
158, 9, 12, 14syl3anc 1491 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ∈ (Clsd‘𝐽))
16 simp1rr 1321 . . . . . . 7 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽 ∧ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)) → 𝑦𝑥)
174adantr 473 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽) → 𝑥𝐽)
18 elequ2 2171 . . . . . . . . . . 11 (𝑏 = 𝑥 → (𝑎𝑏𝑎𝑥))
19 elequ2 2171 . . . . . . . . . . 11 (𝑏 = 𝑥 → (𝑦𝑏𝑦𝑥))
2018, 19bibi12d 337 . . . . . . . . . 10 (𝑏 = 𝑥 → ((𝑎𝑏𝑦𝑏) ↔ (𝑎𝑥𝑦𝑥)))
2120rspcv 3491 . . . . . . . . 9 (𝑥𝐽 → (∀𝑏𝐽 (𝑎𝑏𝑦𝑏) → (𝑎𝑥𝑦𝑥)))
2217, 21syl 17 . . . . . . . 8 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽) → (∀𝑏𝐽 (𝑎𝑏𝑦𝑏) → (𝑎𝑥𝑦𝑥)))
23223impia 1146 . . . . . . 7 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽 ∧ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)) → (𝑎𝑥𝑦𝑥))
2416, 23mpbird 249 . . . . . 6 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽 ∧ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)) → 𝑎𝑥)
2524rabssdv 3876 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑥)
26 nrmsep3 21485 . . . . 5 ((𝐽 ∈ Nrm ∧ (𝑥𝐽 ∧ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ∈ (Clsd‘𝐽) ∧ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑥)) → ∃𝑧𝐽 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
273, 4, 15, 25, 26syl13anc 1492 . . . 4 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ∃𝑧𝐽 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
28 biidd 254 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (𝑦𝑏𝑦𝑏))
2928ralrimivw 3146 . . . . . . . 8 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ∀𝑏𝐽 (𝑦𝑏𝑦𝑏))
30 elequ1 2164 . . . . . . . . . . 11 (𝑎 = 𝑦 → (𝑎𝑏𝑦𝑏))
3130bibi1d 335 . . . . . . . . . 10 (𝑎 = 𝑦 → ((𝑎𝑏𝑦𝑏) ↔ (𝑦𝑏𝑦𝑏)))
3231ralbidv 3165 . . . . . . . . 9 (𝑎 = 𝑦 → (∀𝑏𝐽 (𝑎𝑏𝑦𝑏) ↔ ∀𝑏𝐽 (𝑦𝑏𝑦𝑏)))
3332elrab 3554 . . . . . . . 8 (𝑦 ∈ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ↔ (𝑦 𝐽 ∧ ∀𝑏𝐽 (𝑦𝑏𝑦𝑏)))
3412, 29, 33sylanbrc 579 . . . . . . 7 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑦 ∈ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)})
35 ssel 3790 . . . . . . 7 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 → (𝑦 ∈ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} → 𝑦𝑧))
3634, 35syl5com 31 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧𝑦𝑧))
3736anim1d 605 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
3837reximdv 3194 . . . 4 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (∃𝑧𝐽 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → ∃𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
3927, 38mpd 15 . . 3 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ∃𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
4039ralrimivva 3150 . 2 ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
41 isreg 21462 . 2 (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
422, 40, 41sylanbrc 579 1 ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Reg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108  wcel 2157  wral 3087  wrex 3088  {crab 3091  wss 3767   cuni 4626  cmpt 4920  cfv 6099  Topctop 21023  TopOnctopon 21040  Clsdccld 21146  clsccl 21148  Frect1 21437  Regcreg 21439  Nrmcnrm 21440  KQckq 21822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-rex 3093  df-reu 3094  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-id 5218  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-map 8095  df-qtop 16479  df-top 21024  df-topon 21041  df-cld 21149  df-cn 21357  df-t1 21444  df-reg 21446  df-nrm 21447  df-kq 21823
This theorem is referenced by:  nrmreg  21953
  Copyright terms: Public domain W3C validator