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

Metamath Proof Explorer

Theorem lfinpfin

Description: A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion lfinpfin ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝐴 ∈ PtFin )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
3 1 2 locfinbas ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → ∪ 𝐽 = ∪ 𝐴 )
4 3 eleq2d ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → ( 𝑥 ∈ ∪ 𝐽 ↔ 𝑥 ∈ ∪ 𝐴 ) )
5 4 biimpar ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) → 𝑥 ∈ ∪ 𝐽 )
6 1 locfinnei ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
7 5 6 syldan ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
8 inelcm ⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑥 ∈ 𝑛 ) → ( 𝑠 ∩ 𝑛 ) ≠ ∅ )
9 8 expcom ⊢ ( 𝑥 ∈ 𝑛 → ( 𝑥 ∈ 𝑠 → ( 𝑠 ∩ 𝑛 ) ≠ ∅ ) )
10 9 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑥 ∈ 𝑛 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑠 → ( 𝑠 ∩ 𝑛 ) ≠ ∅ ) )
11 10 ss2rabdv ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑥 ∈ 𝑛 ) → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ⊆ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } )
12 ssfi ⊢ ( ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ∧ { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ⊆ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ) → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin )
13 12 expcom ⊢ ( { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ⊆ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } → ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) )
14 11 13 syl ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑥 ∈ 𝑛 ) → ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) )
15 14 expimpd ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) → ( ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) )
16 15 rexlimdvw ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) → ( ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) )
17 7 16 mpd ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐴 ) → { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin )
18 17 ralrimiva ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → ∀ 𝑥 ∈ ∪ 𝐴 { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin )
19 2 isptfin ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → ( 𝐴 ∈ PtFin ↔ ∀ 𝑥 ∈ ∪ 𝐴 { 𝑠 ∈ 𝐴 ∣ 𝑥 ∈ 𝑠 } ∈ Fin ) )
20 18 19 mpbird ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝐴 ∈ PtFin )