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 ‘ 𝒫 𝑋 ) )