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

Theorem dissnlocfin 22896
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 22361 . 2 (𝑋 ∈ 𝑉 β†’ 𝒫 𝑋 ∈ Top)
2 eqidd 2738 . 2 (𝑋 ∈ 𝑉 β†’ 𝑋 = 𝑋)
3 snelpwi 5405 . . . . 5 (𝑧 ∈ 𝑋 β†’ {𝑧} ∈ 𝒫 𝑋)
43adantl 483 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑧} ∈ 𝒫 𝑋)
5 vsnid 4628 . . . . 5 𝑧 ∈ {𝑧}
65a1i 11 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ 𝑧 ∈ {𝑧})
7 nfv 1918 . . . . . 6 Ⅎ𝑒(𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋)
8 nfrab1 3429 . . . . . 6 Ⅎ𝑒{𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…}
9 nfcv 2908 . . . . . 6 Ⅎ𝑒{{𝑧}}
10 dissnref.c . . . . . . . . . 10 𝐢 = {𝑒 ∣ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}}
1110eqabi 2882 . . . . . . . . 9 (𝑒 ∈ 𝐢 ↔ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
1211anbi1i 625 . . . . . . . 8 ((𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
13 simpr 486 . . . . . . . . . . . . 13 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ 𝑒 = {π‘₯})
14 simplr 768 . . . . . . . . . . . . . . . . . 18 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ 𝑒 = {π‘₯})
1514ineq1d 4176 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) = ({π‘₯} ∩ {𝑧}))
16 disjsn2 4678 . . . . . . . . . . . . . . . . . 18 (π‘₯ β‰  𝑧 β†’ ({π‘₯} ∩ {𝑧}) = βˆ…)
1716adantl 483 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ ({π‘₯} ∩ {𝑧}) = βˆ…)
1815, 17eqtrd 2777 . . . . . . . . . . . . . . . 16 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) = βˆ…)
19 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ (𝑒 ∩ {𝑧}) β‰  βˆ…)
2019neneqd 2949 . . . . . . . . . . . . . . . 16 ((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) ∧ π‘₯ β‰  𝑧) β†’ Β¬ (𝑒 ∩ {𝑧}) = βˆ…)
2118, 20pm2.65da 816 . . . . . . . . . . . . . . 15 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ Β¬ π‘₯ β‰  𝑧)
22 nne 2948 . . . . . . . . . . . . . . 15 (Β¬ π‘₯ β‰  𝑧 ↔ π‘₯ = 𝑧)
2321, 22sylib 217 . . . . . . . . . . . . . 14 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ π‘₯ = 𝑧)
2423sneqd 4603 . . . . . . . . . . . . 13 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ {π‘₯} = {𝑧})
2513, 24eqtrd 2777 . . . . . . . . . . . 12 (((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ π‘₯ ∈ 𝑋) ∧ 𝑒 = {π‘₯}) β†’ 𝑒 = {𝑧})
2625r19.29an 3156 . . . . . . . . . . 11 ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}) β†’ 𝑒 = {𝑧})
2726an32s 651 . . . . . . . . . 10 ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯}) ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) β†’ 𝑒 = {𝑧})
2827anasss 468 . . . . . . . . 9 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…)) β†’ 𝑒 = {𝑧})
29 sneq 4601 . . . . . . . . . . . 12 (π‘₯ = 𝑧 β†’ {π‘₯} = {𝑧})
3029rspceeqv 3600 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ∧ 𝑒 = {𝑧}) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
3130adantll 713 . . . . . . . . . 10 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯})
32 simpr 486 . . . . . . . . . . . . 13 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ 𝑒 = {𝑧})
3332ineq1d 4176 . . . . . . . . . . . 12 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) = ({𝑧} ∩ {𝑧}))
34 inidm 4183 . . . . . . . . . . . 12 ({𝑧} ∩ {𝑧}) = {𝑧}
3533, 34eqtrdi 2793 . . . . . . . . . . 11 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) = {𝑧})
36 vex 3452 . . . . . . . . . . . . 13 𝑧 ∈ V
3736snnz 4742 . . . . . . . . . . . 12 {𝑧} β‰  βˆ…
3837a1i 11 . . . . . . . . . . 11 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ {𝑧} β‰  βˆ…)
3935, 38eqnetrd 3012 . . . . . . . . . 10 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (𝑒 ∩ {𝑧}) β‰  βˆ…)
4031, 39jca 513 . . . . . . . . 9 (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑒 = {𝑧}) β†’ (βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
4128, 40impbida 800 . . . . . . . 8 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ ((βˆƒπ‘₯ ∈ 𝑋 𝑒 = {π‘₯} ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ 𝑒 = {𝑧}))
4212, 41bitrid 283 . . . . . . 7 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ ((𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…) ↔ 𝑒 = {𝑧}))
43 rabid 3430 . . . . . . 7 (𝑒 ∈ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ↔ (𝑒 ∈ 𝐢 ∧ (𝑒 ∩ {𝑧}) β‰  βˆ…))
44 velsn 4607 . . . . . . 7 (𝑒 ∈ {{𝑧}} ↔ 𝑒 = {𝑧})
4542, 43, 443bitr4g 314 . . . . . 6 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ (𝑒 ∈ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ↔ 𝑒 ∈ {{𝑧}}))
467, 8, 9, 45eqrd 3968 . . . . 5 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} = {{𝑧}})
47 snfi 8995 . . . . 5 {{𝑧}} ∈ Fin
4846, 47eqeltrdi 2846 . . . 4 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)
49 eleq2 2827 . . . . . 6 (𝑦 = {𝑧} β†’ (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑧}))
50 ineq2 4171 . . . . . . . . 9 (𝑦 = {𝑧} β†’ (𝑒 ∩ 𝑦) = (𝑒 ∩ {𝑧}))
5150neeq1d 3004 . . . . . . . 8 (𝑦 = {𝑧} β†’ ((𝑒 ∩ 𝑦) β‰  βˆ… ↔ (𝑒 ∩ {𝑧}) β‰  βˆ…))
5251rabbidv 3418 . . . . . . 7 (𝑦 = {𝑧} β†’ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} = {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…})
5352eleq1d 2823 . . . . . 6 (𝑦 = {𝑧} β†’ ({𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin ↔ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin))
5449, 53anbi12d 632 . . . . 5 (𝑦 = {𝑧} β†’ ((𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin) ↔ (𝑧 ∈ {𝑧} ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)))
5554rspcev 3584 . . . 4 (({𝑧} ∈ 𝒫 𝑋 ∧ (𝑧 ∈ {𝑧} ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ {𝑧}) β‰  βˆ…} ∈ Fin)) β†’ βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
564, 6, 48, 55syl12anc 836 . . 3 ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
5756ralrimiva 3144 . 2 (𝑋 ∈ 𝑉 β†’ βˆ€π‘§ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin))
58 unipw 5412 . . . 4 βˆͺ 𝒫 𝑋 = 𝑋
5958eqcomi 2746 . . 3 𝑋 = βˆͺ 𝒫 𝑋
6010unisngl 22894 . . 3 𝑋 = βˆͺ 𝐢
6159, 60islocfin 22884 . 2 (𝐢 ∈ (LocFinβ€˜π’« 𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ βˆ€π‘§ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑒 ∈ 𝐢 ∣ (𝑒 ∩ 𝑦) β‰  βˆ…} ∈ Fin)))
621, 2, 57, 61syl3anbrc 1344 1 (𝑋 ∈ 𝑉 β†’ 𝐢 ∈ (LocFinβ€˜π’« 𝑋))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2714   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410   ∩ cin 3914  βˆ…c0 4287  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870  β€˜cfv 6501  Fincfn 8890  Topctop 22258  LocFinclocfin 22871
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 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-om 7808  df-1o 8417  df-en 8891  df-fin 8894  df-top 22259  df-locfin 22874
This theorem is referenced by:  dispcmp  32480
  Copyright terms: Public domain W3C validator