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

Theorem nrmr0reg 21600
 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 21188 . . 3 (𝐽 ∈ Nrm → 𝐽 ∈ Top)
21adantr 480 . 2 ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Top)
3 simpll 805 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝐽 ∈ Nrm)
4 simprl 809 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑥𝐽)
52adantr 480 . . . . . . 7 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝐽 ∈ Top)
6 eqid 2651 . . . . . . . 8 𝐽 = 𝐽
76toptopon 20770 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
85, 7sylib 208 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝐽 ∈ (TopOn‘ 𝐽))
9 simplr 807 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (KQ‘𝐽) ∈ Fre)
10 simprr 811 . . . . . . 7 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑦𝑥)
11 elunii 4473 . . . . . . 7 ((𝑦𝑥𝑥𝐽) → 𝑦 𝐽)
1210, 4, 11syl2anc 694 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑦 𝐽)
13 eqid 2651 . . . . . . 7 (𝑧 𝐽 ↦ {𝑤𝐽𝑧𝑤}) = (𝑧 𝐽 ↦ {𝑤𝐽𝑧𝑤})
1413r0cld 21589 . . . . . 6 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝑦 𝐽) → {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ∈ (Clsd‘𝐽))
158, 9, 12, 14syl3anc 1366 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ∈ (Clsd‘𝐽))
16 simp1rr 1147 . . . . . . 7 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽 ∧ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)) → 𝑦𝑥)
174adantr 480 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽) → 𝑥𝐽)
18 elequ2 2044 . . . . . . . . . . 11 (𝑏 = 𝑥 → (𝑎𝑏𝑎𝑥))
19 elequ2 2044 . . . . . . . . . . 11 (𝑏 = 𝑥 → (𝑦𝑏𝑦𝑥))
2018, 19bibi12d 334 . . . . . . . . . 10 (𝑏 = 𝑥 → ((𝑎𝑏𝑦𝑏) ↔ (𝑎𝑥𝑦𝑥)))
2120rspcv 3336 . . . . . . . . 9 (𝑥𝐽 → (∀𝑏𝐽 (𝑎𝑏𝑦𝑏) → (𝑎𝑥𝑦𝑥)))
2217, 21syl 17 . . . . . . . 8 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽) → (∀𝑏𝐽 (𝑎𝑏𝑦𝑏) → (𝑎𝑥𝑦𝑥)))
23223impia 1280 . . . . . . 7 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽 ∧ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)) → (𝑎𝑥𝑦𝑥))
2416, 23mpbird 247 . . . . . 6 ((((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) ∧ 𝑎 𝐽 ∧ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)) → 𝑎𝑥)
2524rabssdv 3715 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑥)
26 nrmsep3 21207 . . . . 5 ((𝐽 ∈ Nrm ∧ (𝑥𝐽 ∧ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ∈ (Clsd‘𝐽) ∧ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑥)) → ∃𝑧𝐽 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
273, 4, 15, 25, 26syl13anc 1368 . . . 4 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ∃𝑧𝐽 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
28 biidd 252 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (𝑦𝑏𝑦𝑏))
2928ralrimivw 2996 . . . . . . . 8 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ∀𝑏𝐽 (𝑦𝑏𝑦𝑏))
30 elequ1 2037 . . . . . . . . . . 11 (𝑎 = 𝑦 → (𝑎𝑏𝑦𝑏))
3130bibi1d 332 . . . . . . . . . 10 (𝑎 = 𝑦 → ((𝑎𝑏𝑦𝑏) ↔ (𝑦𝑏𝑦𝑏)))
3231ralbidv 3015 . . . . . . . . 9 (𝑎 = 𝑦 → (∀𝑏𝐽 (𝑎𝑏𝑦𝑏) ↔ ∀𝑏𝐽 (𝑦𝑏𝑦𝑏)))
3332elrab 3396 . . . . . . . 8 (𝑦 ∈ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ↔ (𝑦 𝐽 ∧ ∀𝑏𝐽 (𝑦𝑏𝑦𝑏)))
3412, 29, 33sylanbrc 699 . . . . . . 7 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → 𝑦 ∈ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)})
35 ssel 3630 . . . . . . 7 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 → (𝑦 ∈ {𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} → 𝑦𝑧))
3634, 35syl5com 31 . . . . . 6 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧𝑦𝑧))
3736anim1d 587 . . . . 5 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
3837reximdv 3045 . . . 4 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → (∃𝑧𝐽 ({𝑎 𝐽 ∣ ∀𝑏𝐽 (𝑎𝑏𝑦𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → ∃𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
3927, 38mpd 15 . . 3 (((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝑥𝐽𝑦𝑥)) → ∃𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
4039ralrimivva 3000 . 2 ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))
41 isreg 21184 . 2 (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥𝐽𝑦𝑥𝑧𝐽 (𝑦𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
422, 40, 41sylanbrc 699 1 ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Reg)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  {crab 2945   ⊆ wss 3607  ∪ cuni 4468   ↦ cmpt 4762  ‘cfv 5926  Topctop 20746  TopOnctopon 20763  Clsdccld 20868  clsccl 20870  Frect1 21159  Regcreg 21161  Nrmcnrm 21162  KQckq 21544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-map 7901  df-qtop 16214  df-top 20747  df-topon 20764  df-cld 20871  df-cn 21079  df-t1 21166  df-reg 21168  df-nrm 21169  df-kq 21545 This theorem is referenced by:  nrmreg  21675
 Copyright terms: Public domain W3C validator