Theorem finlocfin

Description: A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010)

	Ref	Expression
Hypotheses	finlocfin.1	⊢ 𝑋 = ∪ 𝐽
	finlocfin.2	⊢ 𝑌 = ∪ 𝐴
Assertion	finlocfin	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝐴 ∈ ( LocFin ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		finlocfin.1	⊢ 𝑋 = ∪ 𝐽
2		finlocfin.2	⊢ 𝑌 = ∪ 𝐴
3		simp1	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝐽 ∈ Top )
4		simp3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
5		simpl1	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ Top )
6	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
7	5 6	syl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ 𝐽 )
8		simpr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
9		simpl2	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ Fin )
10		ssrab2	⊢ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ⊆ 𝐴
11		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ⊆ 𝐴 ) → { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ∈ Fin )
12	9 10 11	sylancl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ∈ Fin )
13		eleq2	⊢ ( 𝑛 = 𝑋 → ( 𝑥 ∈ 𝑛 ↔ 𝑥 ∈ 𝑋 ) )
14		ineq2	⊢ ( 𝑛 = 𝑋 → ( 𝑠 ∩ 𝑛 ) = ( 𝑠 ∩ 𝑋 ) )
15	14	neeq1d	⊢ ( 𝑛 = 𝑋 → ( ( 𝑠 ∩ 𝑛 ) ≠ ∅ ↔ ( 𝑠 ∩ 𝑋 ) ≠ ∅ ) )
16	15	rabbidv	⊢ ( 𝑛 = 𝑋 → { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } = { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } )
17	16	eleq1d	⊢ ( 𝑛 = 𝑋 → ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ↔ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) )
18	13 17	anbi12d	⊢ ( 𝑛 = 𝑋 → ( ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ( 𝑥 ∈ 𝑋 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ) )
19	18	rspcev	⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑋 ) ≠ ∅ } ∈ Fin ) ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
20	7 8 12 19	syl12anc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
21	20	ralrimiva	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
22	1 2	islocfin	⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
23	3 4 21 22	syl3anbrc	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝐴 ∈ ( LocFin ‘ 𝐽 ) )