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

Theorem dissnlocfin 23024
Description: The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.)
Hypothesis
Ref Expression
dissnref.c 𝐢 = {𝑒 ∣ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}}
Assertion
Ref Expression
dissnlocfin (𝑋 ∈ 𝑉 β†’ 𝐢 ∈ (LocFinβ€˜π’« 𝑋))
Distinct variable groups:   𝑒,𝐢,π‘₯   𝑒,𝑉,π‘₯   𝑒,𝑋,π‘₯

Proof of Theorem dissnlocfin
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 distop 22489 . 2 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ Top)
2 eqidd 2733 . 2 (𝑋 ∈ 𝑉 β†’ 𝑋 = 𝑋)
3 snelpwi 5442 . . . . 5 (𝑧 ∈ 𝑋 β†’ {𝑧} ∈ 𝒫 𝑋)
43adantl 482 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑧} ∈ 𝒫 𝑋)
5 vsnid 4664 . . . . 5 𝑧 ∈ {𝑧}
65a1i 11 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ 𝑧 ∈ {𝑧})
7 nfv 1917 . . . . . 6 Ⅎ𝑒(𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋)
8 nfrab1 3451 . . . . . 6 Ⅎ𝑒{𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…}
9 nfcv 2903 . . . . . 6 Ⅎ𝑒{{𝑧}}
10 dissnref.c . . . . . . . . . 10 𝐢 = {𝑒 ∣ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}}
1110eqabri 2877 . . . . . . . . 9 (𝑒 ∈ 𝐢 ↔ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
1211anbi1i 624 . . . . . . . 8 ((𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
13 simpr 485 . . . . . . . . . . . . 13 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ 𝑒 = {π‘₯})
14 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ 𝑒 = {π‘₯})
1514ineq1d 4210 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) = ({π‘₯} ∩ {𝑧}))
16 disjsn2 4715 . . . . . . . . . . . . . . . . . 18 (π‘₯ β‰  𝑧 β†’ ({π‘₯} ∩ {𝑧}) = βˆ…)
1716adantl 482 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ ({π‘₯} ∩ {𝑧}) = βˆ…)
1815, 17eqtrd 2772 . . . . . . . . . . . . . . . 16 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) = βˆ…)
19 simp-4r 782 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) β‰  βˆ…)
2019neneqd 2945 . . . . . . . . . . . . . . . 16 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ Β¬ (𝑒 ∩ {𝑧}) = βˆ…)
2118, 20pm2.65da 815 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ Β¬ π‘₯ β‰  𝑧)
22 nne 2944 . . . . . . . . . . . . . . 15 (Β¬ π‘₯ β‰  𝑧 ↔ π‘₯ = 𝑧)
2321, 22sylib 217 . . . . . . . . . . . . . 14 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ π‘₯ = 𝑧)
2423sneqd 4639 . . . . . . . . . . . . 13 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ {π‘₯} = {𝑧})
2513, 24eqtrd 2772 . . . . . . . . . . . 12 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ 𝑒 = {𝑧})
2625r19.29an 3158 . . . . . . . . . . 11 ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}) β†’ 𝑒 = {𝑧})
2726an32s 650 . . . . . . . . . 10 ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) β†’ 𝑒 = {𝑧})
2827anasss 467 . . . . . . . . 9 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…)) β†’ 𝑒 = {𝑧})
29 sneq 4637 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ {π‘₯} = {𝑧})
3029rspceeqv 3632 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ∧ 𝑒 = {𝑧}) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
3130adantll 712 . . . . . . . . . 10 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
32 simpr 485 . . . . . . . . . . . . 13 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ 𝑒 = {𝑧})
3332ineq1d 4210 . . . . . . . . . . . 12 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) = ({𝑧} ∩ {𝑧}))
34 inidm 4217 . . . . . . . . . . . 12 ({𝑧} ∩ {𝑧}) = {𝑧}
3533, 34eqtrdi 2788 . . . . . . . . . . 11 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) = {𝑧})
36 vex 3478 . . . . . . . . . . . . 13 𝑧 ∈ V
3736snnz 4779 . . . . . . . . . . . 12 {𝑧} β‰  βˆ…
3837a1i 11 . . . . . . . . . . 11 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ {𝑧} β‰  βˆ…)
3935, 38eqnetrd 3008 . . . . . . . . . 10 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) β‰  βˆ…)
4031, 39jca 512 . . . . . . . . 9 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
4128, 40impbida 799 . . . . . . . 8 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ ((βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ 𝑒 = {𝑧}))
4212, 41bitrid 282 . . . . . . 7 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ ((𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ 𝑒 = {𝑧}))
43 rabid 3452 . . . . . . 7 (𝑒 ∈ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ↔ (𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
44 velsn 4643 . . . . . . 7 (𝑒 ∈ {{𝑧}} ↔ 𝑒 = {𝑧})
4542, 43, 443bitr4g 313 . . . . . 6 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ (𝑒 ∈ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ↔ 𝑒 ∈ {{𝑧}}))
467, 8, 9, 45eqrd 4000 . . . . 5 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} = {{𝑧}})
47 snfi 9040 . . . . 5 {{𝑧}} ∈ Fin
4846, 47eqeltrdi 2841 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)
49 eleq2 2822 . . . . . 6 (𝑦 = {𝑧} β†’ (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑧}))
50 ineq2 4205 . . . . . . . . 9 (𝑦 = {𝑧} β†’ (𝑒 ∩ 𝑦) = (𝑒 ∩ {𝑧}))
5150neeq1d 3000 . . . . . . . 8 (𝑦 = {𝑧} β†’ ((𝑒 ∩ 𝑦) β‰  βˆ… ↔ (𝑒 ∩ {𝑧}) β‰  βˆ…))
5251rabbidv 3440 . . . . . . 7 (𝑦 = {𝑧} β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} = {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…})
5352eleq1d 2818 . . . . . 6 (𝑦 = {𝑧} β†’ ({𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin ↔ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin))
5449, 53anbi12d 631 . . . . 5 (𝑦 = {𝑧} β†’ ((𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin) ↔ (𝑧 ∈ {𝑧} ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)))
5554rspcev 3612 . . . 4 (({𝑧} ∈ 𝒫 𝑋 ∧ (𝑧 ∈ {𝑧} ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)) β†’ βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
564, 6, 48, 55syl12anc 835 . . 3 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
5756ralrimiva 3146 . 2 (𝑋 ∈ 𝑉 β†’ βˆ€π‘§ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
58 unipw 5449 . . . 4 βˆͺ 𝒫 𝑋 = 𝑋
5958eqcomi 2741 . . 3 𝑋 = βˆͺ 𝒫 𝑋
6010unisngl 23022 . . 3 𝑋 = βˆͺ 𝐢
6159, 60islocfin 23012 . 2 (𝐢 ∈ (LocFinβ€˜π’« 𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ βˆ€π‘§ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin)))
621, 2, 57, 61syl3anbrc 1343 1 (𝑋 ∈ 𝑉 β†’ 𝐢 ∈ (LocFinβ€˜π’« 𝑋))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   ∩ cin 3946  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  β€˜cfv 6540  Fincfn 8935  Topctop 22386  LocFinclocfin 22999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  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-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  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-om 7852  df-1o 8462  df-en 8936  df-fin 8939  df-top 22387  df-locfin 23002
This theorem is referenced by:  dispcmp  32827
  Copyright terms: Public domain W3C validator