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

Theorem r0cld 23224
Description: The analogue of the T1 axiom (singletons are closed) for an R0 space. In an R0 space the set of all points topologically indistinguishable from 𝐴 is closed. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
Assertion
Ref Expression
r0cld ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → {𝑧𝑋 ∣ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)} ∈ (Clsd‘𝐽))
Distinct variable groups:   𝑥,𝑜,𝑦,𝑧,𝐴   𝑜,𝐽,𝑥,𝑦,𝑧   𝑜,𝐹,𝑧   𝑜,𝑋,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem r0cld
StepHypRef Expression
1 kqval.2 . . . . . 6 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
21kqffn 23211 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
323ad2ant1 1134 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → 𝐹 Fn 𝑋)
4 fncnvima2 7058 . . . 4 (𝐹 Fn 𝑋 → (𝐹 “ {(𝐹𝐴)}) = {𝑧𝑋 ∣ (𝐹𝑧) ∈ {(𝐹𝐴)}})
53, 4syl 17 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (𝐹 “ {(𝐹𝐴)}) = {𝑧𝑋 ∣ (𝐹𝑧) ∈ {(𝐹𝐴)}})
6 fvex 6901 . . . . . 6 (𝐹𝑧) ∈ V
76elsn 4642 . . . . 5 ((𝐹𝑧) ∈ {(𝐹𝐴)} ↔ (𝐹𝑧) = (𝐹𝐴))
8 simpl1 1192 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) ∧ 𝑧𝑋) → 𝐽 ∈ (TopOn‘𝑋))
9 simpr 486 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) ∧ 𝑧𝑋) → 𝑧𝑋)
10 simpl3 1194 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) ∧ 𝑧𝑋) → 𝐴𝑋)
111kqfeq 23210 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝐴𝑋) → ((𝐹𝑧) = (𝐹𝐴) ↔ ∀𝑦𝐽 (𝑧𝑦𝐴𝑦)))
12 eleq2w 2818 . . . . . . . . 9 (𝑦 = 𝑜 → (𝑧𝑦𝑧𝑜))
13 eleq2w 2818 . . . . . . . . 9 (𝑦 = 𝑜 → (𝐴𝑦𝐴𝑜))
1412, 13bibi12d 346 . . . . . . . 8 (𝑦 = 𝑜 → ((𝑧𝑦𝐴𝑦) ↔ (𝑧𝑜𝐴𝑜)))
1514cbvralvw 3235 . . . . . . 7 (∀𝑦𝐽 (𝑧𝑦𝐴𝑦) ↔ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜))
1611, 15bitrdi 287 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝑋𝐴𝑋) → ((𝐹𝑧) = (𝐹𝐴) ↔ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)))
178, 9, 10, 16syl3anc 1372 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) ∧ 𝑧𝑋) → ((𝐹𝑧) = (𝐹𝐴) ↔ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)))
187, 17bitrid 283 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ {(𝐹𝐴)} ↔ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)))
1918rabbidva 3440 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → {𝑧𝑋 ∣ (𝐹𝑧) ∈ {(𝐹𝐴)}} = {𝑧𝑋 ∣ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)})
205, 19eqtrd 2773 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (𝐹 “ {(𝐹𝐴)}) = {𝑧𝑋 ∣ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)})
211kqid 23214 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
22213ad2ant1 1134 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
23 simp2 1138 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (KQ‘𝐽) ∈ Fre)
24 simp3 1139 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → 𝐴𝑋)
25 fnfvelrn 7078 . . . . . 6 ((𝐹 Fn 𝑋𝐴𝑋) → (𝐹𝐴) ∈ ran 𝐹)
263, 24, 25syl2anc 585 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (𝐹𝐴) ∈ ran 𝐹)
271kqtopon 23213 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
28273ad2ant1 1134 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
29 toponuni 22398 . . . . . 6 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = (KQ‘𝐽))
3028, 29syl 17 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → ran 𝐹 = (KQ‘𝐽))
3126, 30eleqtrd 2836 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (𝐹𝐴) ∈ (KQ‘𝐽))
32 eqid 2733 . . . . 5 (KQ‘𝐽) = (KQ‘𝐽)
3332t1sncld 22812 . . . 4 (((KQ‘𝐽) ∈ Fre ∧ (𝐹𝐴) ∈ (KQ‘𝐽)) → {(𝐹𝐴)} ∈ (Clsd‘(KQ‘𝐽)))
3423, 31, 33syl2anc 585 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → {(𝐹𝐴)} ∈ (Clsd‘(KQ‘𝐽)))
35 cnclima 22754 . . 3 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ {(𝐹𝐴)} ∈ (Clsd‘(KQ‘𝐽))) → (𝐹 “ {(𝐹𝐴)}) ∈ (Clsd‘𝐽))
3622, 34, 35syl2anc 585 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → (𝐹 “ {(𝐹𝐴)}) ∈ (Clsd‘𝐽))
3720, 36eqeltrrd 2835 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴𝑋) → {𝑧𝑋 ∣ ∀𝑜𝐽 (𝑧𝑜𝐴𝑜)} ∈ (Clsd‘𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062  {crab 3433  {csn 4627   cuni 4907  cmpt 5230  ccnv 5674  ran crn 5676  cima 5678   Fn wfn 6535  cfv 6540  (class class class)co 7404  TopOnctopon 22394  Clsdccld 22502   Cn ccn 22710  Frect1 22793  KQckq 23179
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-map 8818  df-qtop 17449  df-top 22378  df-topon 22395  df-cld 22505  df-cn 22713  df-t1 22800  df-kq 23180
This theorem is referenced by:  nrmr0reg  23235
  Copyright terms: Public domain W3C validator