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 )