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

Metamath Proof Explorer

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 ∧ 𝑋 = 𝑌 ) )