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

Metamath Proof Explorer

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 ‘ 𝐽 ) )