Metamath Proof Explorer

Theorem locfincf

Description: A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis locfincf.1 ⊢ 𝑋 = ∪ 𝐽
Assertion locfincf ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( LocFin ‘ 𝐽 ) ⊆ ( LocFin ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 locfincf.1 ⊢ 𝑋 = ∪ 𝐽
2 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝐾 ∈ Top )
3 2 ad2antrr ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → 𝐾 ∈ Top )
4 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐾 )
5 4 ad2antrr ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → 𝑋 = ∪ 𝐾 )
6 eqid ⊢ ∪ 𝑥 = ∪ 𝑥
7 1 6 locfinbas ⊢ ( 𝑥 ∈ ( LocFin ‘ 𝐽 ) → 𝑋 = ∪ 𝑥 )
8 7 adantl ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → 𝑋 = ∪ 𝑥 )
9 5 8 eqtr3d ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → ∪ 𝐾 = ∪ 𝑥 )
10 5 eleq2d ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → ( 𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ 𝐾 ) )
11 1 locfinnei ⊢ ( ( 𝑥 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
12 11 ex ⊢ ( 𝑥 ∈ ( LocFin ‘ 𝐽 ) → ( 𝑦 ∈ 𝑋 → ∃ 𝑛 ∈ 𝐽 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
13 ssrexv ⊢ ( 𝐽 ⊆ 𝐾 → ( ∃ 𝑛 ∈ 𝐽 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → ∃ 𝑛 ∈ 𝐾 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
14 13 adantl ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ∃ 𝑛 ∈ 𝐽 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → ∃ 𝑛 ∈ 𝐾 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
15 12 14 sylan9r ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → ( 𝑦 ∈ 𝑋 → ∃ 𝑛 ∈ 𝐾 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
16 10 15 sylbird ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → ( 𝑦 ∈ ∪ 𝐾 → ∃ 𝑛 ∈ 𝐾 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
17 16 ralrimiv ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → ∀ 𝑦 ∈ ∪ 𝐾 ∃ 𝑛 ∈ 𝐾 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
18 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
19 18 6 islocfin ⊢ ( 𝑥 ∈ ( LocFin ‘ 𝐾 ) ↔ ( 𝐾 ∈ Top ∧ ∪ 𝐾 = ∪ 𝑥 ∧ ∀ 𝑦 ∈ ∪ 𝐾 ∃ 𝑛 ∈ 𝐾 ( 𝑦 ∈ 𝑛 ∧ { 𝑠 ∈ 𝑥 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
20 3 9 17 19 syl3anbrc ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( LocFin ‘ 𝐽 ) ) → 𝑥 ∈ ( LocFin ‘ 𝐾 ) )
21 20 ex ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( LocFin ‘ 𝐽 ) → 𝑥 ∈ ( LocFin ‘ 𝐾 ) ) )
22 21 ssrdv ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( LocFin ‘ 𝐽 ) ⊆ ( LocFin ‘ 𝐾 ) )