Theorem locfindis

Description: The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypothesis	locfindis.1	⊢ 𝑌 = ∪ 𝐶
Assertion	locfindis	⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) ↔ ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		locfindis.1	⊢ 𝑌 = ∪ 𝐶
2		lfinpfin	⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) → 𝐶 ∈ PtFin )
3		unipw	⊢ ∪ 𝒫 𝑋 = 𝑋
4	3	eqcomi	⊢ 𝑋 = ∪ 𝒫 𝑋
5	4 1	locfinbas	⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) → 𝑋 = 𝑌 )
6	2 5	jca	⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) → ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) )
7		simpr	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
8		uniexg	⊢ ( 𝐶 ∈ PtFin → ∪ 𝐶 ∈ V )
9	1 8	eqeltrid	⊢ ( 𝐶 ∈ PtFin → 𝑌 ∈ V )
10	9	adantr	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → 𝑌 ∈ V )
11	7 10	eqeltrd	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ V )
12		distop	⊢ ( 𝑋 ∈ V → 𝒫 𝑋 ∈ Top )
13	11 12	syl	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → 𝒫 𝑋 ∈ Top )
14		snelpwi	⊢ ( 𝑥 ∈ 𝑋 → { 𝑥 } ∈ 𝒫 𝑋 )
15	14	adantl	⊢ ( ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝒫 𝑋 )
16		snidg	⊢ ( 𝑥 ∈ 𝑋 → 𝑥 ∈ { 𝑥 } )
17	16	adantl	⊢ ( ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ { 𝑥 } )
18		simpll	⊢ ( ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ PtFin )
19	7	eleq2d	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ 𝑌 ) )
20	19	biimpa	⊢ ( ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑌 )
21	1	ptfinfin	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑥 ∈ 𝑌 ) → { 𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠 } ∈ Fin )
22	18 20 21	syl2anc	⊢ ( ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠 } ∈ Fin )
23		eleq2	⊢ ( 𝑦 = { 𝑥 } → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ { 𝑥 } ) )
24		ineq2	⊢ ( 𝑦 = { 𝑥 } → ( 𝑠 ∩ 𝑦 ) = ( 𝑠 ∩ { 𝑥 } ) )
25	24	neeq1d	⊢ ( 𝑦 = { 𝑥 } → ( ( 𝑠 ∩ 𝑦 ) ≠ ∅ ↔ ( 𝑠 ∩ { 𝑥 } ) ≠ ∅ ) )
26		disjsn	⊢ ( ( 𝑠 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ 𝑠 )
27	26	necon2abii	⊢ ( 𝑥 ∈ 𝑠 ↔ ( 𝑠 ∩ { 𝑥 } ) ≠ ∅ )
28	25 27	bitr4di	⊢ ( 𝑦 = { 𝑥 } → ( ( 𝑠 ∩ 𝑦 ) ≠ ∅ ↔ 𝑥 ∈ 𝑠 ) )
29	28	rabbidv	⊢ ( 𝑦 = { 𝑥 } → { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } = { 𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠 } )
30	29	eleq1d	⊢ ( 𝑦 = { 𝑥 } → ( { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ↔ { 𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) )
31	23 30	anbi12d	⊢ ( 𝑦 = { 𝑥 } → ( ( 𝑥 ∈ 𝑦 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ { 𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) ) )
32	31	rspcev	⊢ ( ( { 𝑥 } ∈ 𝒫 𝑋 ∧ ( 𝑥 ∈ { 𝑥 } ∧ { 𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) ) → ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝑦 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) )
33	15 17 22 32	syl12anc	⊢ ( ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝑦 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) )
34	33	ralrimiva	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝑦 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) )
35	4 1	islocfin	⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) ↔ ( 𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝑦 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑦 ) ≠ ∅ } ∈ Fin ) ) )
36	13 7 34 35	syl3anbrc	⊢ ( ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) → 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) )
37	6 36	impbii	⊢ ( 𝐶 ∈ ( LocFin ‘ 𝒫 𝑋 ) ↔ ( 𝐶 ∈ PtFin ∧ 𝑋 = 𝑌 ) )