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 ⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
Assertion dissnlocfin ( 𝑋 ∈ 𝑉 → 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dissnref.c ⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } }
2 distop ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top )
3 eqidd ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 = 𝑋 )
4 snelpwi ⊢ ( 𝑧 ∈ 𝑋 → { 𝑧 } ∈ 𝒫 𝑋 )
5 4 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → { 𝑧 } ∈ 𝒫 𝑋 )
6 vsnid ⊢ 𝑧 ∈ { 𝑧 }
7 6 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ { 𝑧 } )
8 nfv ⊢ Ⅎ 𝑢 ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 )
9 nfrab1 ⊢ Ⅎ 𝑢 { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ }
10 nfcv ⊢ Ⅎ 𝑢 { { 𝑧 } }
11 1 eqabri ⊢ ( 𝑢 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } )
12 11 anbi1i ⊢ ( ( 𝑢 ∈ 𝐶 ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ↔ ( ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) )
13 simpr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑢 = { 𝑥 } )
14 simplr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ 𝑥 ≠ 𝑧 ) → 𝑢 = { 𝑥 } )
15 14 ineq1d ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ 𝑥 ≠ 𝑧 ) → ( 𝑢 ∩ { 𝑧 } ) = ( { 𝑥 } ∩ { 𝑧 } ) )
16 disjsn2 ⊢ ( 𝑥 ≠ 𝑧 → ( { 𝑥 } ∩ { 𝑧 } ) = ∅ )
17 16 adantl ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ 𝑥 ≠ 𝑧 ) → ( { 𝑥 } ∩ { 𝑧 } ) = ∅ )
18 15 17 eqtrd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ 𝑥 ≠ 𝑧 ) → ( 𝑢 ∩ { 𝑧 } ) = ∅ )
19 simp-4r ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ 𝑥 ≠ 𝑧 ) → ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ )
20 19 neneqd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) ∧ 𝑥 ≠ 𝑧 ) → ¬ ( 𝑢 ∩ { 𝑧 } ) = ∅ )
21 18 20 pm2.65da ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → ¬ 𝑥 ≠ 𝑧 )
22 nne ⊢ ( ¬ 𝑥 ≠ 𝑧 ↔ 𝑥 = 𝑧 )
23 21 22 sylib ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑥 = 𝑧 )
24 23 sneqd ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → { 𝑥 } = { 𝑧 } )
25 13 24 eqtrd ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑢 = { 𝑥 } ) → 𝑢 = { 𝑧 } )
26 25 r19.29an ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ∧ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ) → 𝑢 = { 𝑧 } )
27 26 an32s ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ) ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) → 𝑢 = { 𝑧 } )
28 27 anasss ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ) → 𝑢 = { 𝑧 } )
29 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
30 29 rspceeqv ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑢 = { 𝑧 } ) → ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } )
31 30 adantll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } )
32 simpr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → 𝑢 = { 𝑧 } )
33 32 ineq1d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → ( 𝑢 ∩ { 𝑧 } ) = ( { 𝑧 } ∩ { 𝑧 } ) )
34 inidm ⊢ ( { 𝑧 } ∩ { 𝑧 } ) = { 𝑧 }
35 33 34 eqtrdi ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → ( 𝑢 ∩ { 𝑧 } ) = { 𝑧 } )
36 vex ⊢ 𝑧 ∈ V
37 36 snnz ⊢ { 𝑧 } ≠ ∅
38 37 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → { 𝑧 } ≠ ∅ )
39 35 38 eqnetrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ )
40 31 39 jca ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑢 = { 𝑧 } ) → ( ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) )
41 28 40 impbida ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → ( ( ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ↔ 𝑢 = { 𝑧 } ) )
42 12 41 bitrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑢 ∈ 𝐶 ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) ↔ 𝑢 = { 𝑧 } ) )
43 rabid ⊢ ( 𝑢 ∈ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } ↔ ( 𝑢 ∈ 𝐶 ∧ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) )
44 velsn ⊢ ( 𝑢 ∈ { { 𝑧 } } ↔ 𝑢 = { 𝑧 } )
45 42 43 44 3bitr4g ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑢 ∈ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } ↔ 𝑢 ∈ { { 𝑧 } } ) )
46 8 9 10 45 eqrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } = { { 𝑧 } } )
47 snfi ⊢ { { 𝑧 } } ∈ Fin
48 46 47 eqeltrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } ∈ Fin )
49 eleq2 ⊢ ( 𝑦 = { 𝑧 } → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ { 𝑧 } ) )
50 ineq2 ⊢ ( 𝑦 = { 𝑧 } → ( 𝑢 ∩ 𝑦 ) = ( 𝑢 ∩ { 𝑧 } ) )
51 50 neeq1d ⊢ ( 𝑦 = { 𝑧 } → ( ( 𝑢 ∩ 𝑦 ) ≠ ∅ ↔ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ ) )
52 51 rabbidv ⊢ ( 𝑦 = { 𝑧 } → { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } = { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } )
53 52 eleq1d ⊢ ( 𝑦 = { 𝑧 } → ( { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ↔ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } ∈ Fin ) )
54 49 53 anbi12d ⊢ ( 𝑦 = { 𝑧 } → ( ( 𝑧 ∈ 𝑦 ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) ↔ ( 𝑧 ∈ { 𝑧 } ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } ∈ Fin ) ) )
55 54 rspcev ⊢ ( ( { 𝑧 } ∈ 𝒫 𝑋 ∧ ( 𝑧 ∈ { 𝑧 } ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ { 𝑧 } ) ≠ ∅ } ∈ Fin ) ) → ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑧 ∈ 𝑦 ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) )
56 5 7 48 55 syl12anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑧 ∈ 𝑦 ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) )
57 56 ralrimiva ⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑧 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑧 ∈ 𝑦 ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) )
58 unipw ⊢ ∪ 𝒫 𝑋 = 𝑋
59 58 eqcomi ⊢ 𝑋 = ∪ 𝒫 𝑋
60 1 unisngl ⊢ 𝑋 = ∪ 𝐶
61 59 60 islocfin ⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) ↔ ( 𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑧 ∈ 𝑦 ∧ { 𝑢 ∈ 𝐶 ∣ ( 𝑢 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) ) )
62 2 3 57 61 syl3anbrc ⊢ ( 𝑋 ∈ 𝑉 → 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) )