This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dissnlocfin

Description: The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)

Ref Expression
Hypothesis dissnref.c 
|- C = { u | E. x e. X u = { x } }
Assertion dissnlocfin 
|- ( X e. V -> C e. ( LocFin ` ~P X ) )

Proof

Step Hyp Ref Expression
1 dissnref.c 
 |-  C = { u | E. x e. X u = { x } }
2 distop 
 |-  ( X e. V -> ~P X e. Top )
3 eqidd 
 |-  ( X e. V -> X = X )
4 snelpwi 
 |-  ( z e. X -> { z } e. ~P X )
5 4 adantl 
 |-  ( ( X e. V /\ z e. X ) -> { z } e. ~P X )
6 vsnid 
 |-  z e. { z }
7 6 a1i 
 |-  ( ( X e. V /\ z e. X ) -> z e. { z } )
8 nfv 
 |-  F/ u ( X e. V /\ z e. X )
9 nfrab1 
 |-  F/_ u { u e. C | ( u i^i { z } ) =/= (/) }
10 nfcv 
 |-  F/_ u { { z } }
11 1 eqabri 
 |-  ( u e. C <-> E. x e. X u = { x } )
12 11 anbi1i 
 |-  ( ( u e. C /\ ( u i^i { z } ) =/= (/) ) <-> ( E. x e. X u = { x } /\ ( u i^i { z } ) =/= (/) ) )
13 simpr 
 |-  ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) -> u = { x } )
14 simplr 
 |-  ( ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) /\ x =/= z ) -> u = { x } )
15 14 ineq1d 
 |-  ( ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) /\ x =/= z ) -> ( u i^i { z } ) = ( { x } i^i { z } ) )
16 disjsn2 
 |-  ( x =/= z -> ( { x } i^i { z } ) = (/) )
17 16 adantl 
 |-  ( ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) /\ x =/= z ) -> ( { x } i^i { z } ) = (/) )
18 15 17 eqtrd 
 |-  ( ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) /\ x =/= z ) -> ( u i^i { z } ) = (/) )
19 simp-4r 
 |-  ( ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) /\ x =/= z ) -> ( u i^i { z } ) =/= (/) )
20 19 neneqd 
 |-  ( ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) /\ x =/= z ) -> -. ( u i^i { z } ) = (/) )
21 18 20 pm2.65da 
 |-  ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) -> -. x =/= z )
22 nne 
 |-  ( -. x =/= z <-> x = z )
23 21 22 sylib 
 |-  ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) -> x = z )
24 23 sneqd 
 |-  ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) -> { x } = { z } )
25 13 24 eqtrd 
 |-  ( ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ x e. X ) /\ u = { x } ) -> u = { z } )
26 25 r19.29an 
 |-  ( ( ( ( X e. V /\ z e. X ) /\ ( u i^i { z } ) =/= (/) ) /\ E. x e. X u = { x } ) -> u = { z } )
27 26 an32s 
 |-  ( ( ( ( X e. V /\ z e. X ) /\ E. x e. X u = { x } ) /\ ( u i^i { z } ) =/= (/) ) -> u = { z } )
28 27 anasss 
 |-  ( ( ( X e. V /\ z e. X ) /\ ( E. x e. X u = { x } /\ ( u i^i { z } ) =/= (/) ) ) -> u = { z } )
29 sneq 
 |-  ( x = z -> { x } = { z } )
30 29 rspceeqv 
 |-  ( ( z e. X /\ u = { z } ) -> E. x e. X u = { x } )
31 30 adantll 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> E. x e. X u = { x } )
32 simpr 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> u = { z } )
33 32 ineq1d 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> ( u i^i { z } ) = ( { z } i^i { z } ) )
34 inidm 
 |-  ( { z } i^i { z } ) = { z }
35 33 34 eqtrdi 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> ( u i^i { z } ) = { z } )
36 vex 
 |-  z e. _V
37 36 snnz 
 |-  { z } =/= (/)
38 37 a1i 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> { z } =/= (/) )
39 35 38 eqnetrd 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> ( u i^i { z } ) =/= (/) )
40 31 39 jca 
 |-  ( ( ( X e. V /\ z e. X ) /\ u = { z } ) -> ( E. x e. X u = { x } /\ ( u i^i { z } ) =/= (/) ) )
41 28 40 impbida 
 |-  ( ( X e. V /\ z e. X ) -> ( ( E. x e. X u = { x } /\ ( u i^i { z } ) =/= (/) ) <-> u = { z } ) )
42 12 41 bitrid 
 |-  ( ( X e. V /\ z e. X ) -> ( ( u e. C /\ ( u i^i { z } ) =/= (/) ) <-> u = { z } ) )
43 rabid 
 |-  ( u e. { u e. C | ( u i^i { z } ) =/= (/) } <-> ( u e. C /\ ( u i^i { z } ) =/= (/) ) )
44 velsn 
 |-  ( u e. { { z } } <-> u = { z } )
45 42 43 44 3bitr4g 
 |-  ( ( X e. V /\ z e. X ) -> ( u e. { u e. C | ( u i^i { z } ) =/= (/) } <-> u e. { { z } } ) )
46 8 9 10 45 eqrd 
 |-  ( ( X e. V /\ z e. X ) -> { u e. C | ( u i^i { z } ) =/= (/) } = { { z } } )
47 snfi 
 |-  { { z } } e. Fin
48 46 47 eqeltrdi 
 |-  ( ( X e. V /\ z e. X ) -> { u e. C | ( u i^i { z } ) =/= (/) } e. Fin )
49 eleq2 
 |-  ( y = { z } -> ( z e. y <-> z e. { z } ) )
50 ineq2 
 |-  ( y = { z } -> ( u i^i y ) = ( u i^i { z } ) )
51 50 neeq1d 
 |-  ( y = { z } -> ( ( u i^i y ) =/= (/) <-> ( u i^i { z } ) =/= (/) ) )
52 51 rabbidv 
 |-  ( y = { z } -> { u e. C | ( u i^i y ) =/= (/) } = { u e. C | ( u i^i { z } ) =/= (/) } )
53 52 eleq1d 
 |-  ( y = { z } -> ( { u e. C | ( u i^i y ) =/= (/) } e. Fin <-> { u e. C | ( u i^i { z } ) =/= (/) } e. Fin ) )
54 49 53 anbi12d 
 |-  ( y = { z } -> ( ( z e. y /\ { u e. C | ( u i^i y ) =/= (/) } e. Fin ) <-> ( z e. { z } /\ { u e. C | ( u i^i { z } ) =/= (/) } e. Fin ) ) )
55 54 rspcev 
 |-  ( ( { z } e. ~P X /\ ( z e. { z } /\ { u e. C | ( u i^i { z } ) =/= (/) } e. Fin ) ) -> E. y e. ~P X ( z e. y /\ { u e. C | ( u i^i y ) =/= (/) } e. Fin ) )
56 5 7 48 55 syl12anc 
 |-  ( ( X e. V /\ z e. X ) -> E. y e. ~P X ( z e. y /\ { u e. C | ( u i^i y ) =/= (/) } e. Fin ) )
57 56 ralrimiva 
 |-  ( X e. V -> A. z e. X E. y e. ~P X ( z e. y /\ { u e. C | ( u i^i y ) =/= (/) } e. Fin ) )
58 unipw 
 |-  U. ~P X = X
59 58 eqcomi 
 |-  X = U. ~P X
60 1 unisngl 
 |-  X = U. C
61 59 60 islocfin 
 |-  ( C e. ( LocFin ` ~P X ) <-> ( ~P X e. Top /\ X = X /\ A. z e. X E. y e. ~P X ( z e. y /\ { u e. C | ( u i^i y ) =/= (/) } e. Fin ) ) )
62 2 3 57 61 syl3anbrc 
 |-  ( X e. V -> C e. ( LocFin ` ~P X ) )