Metamath Proof Explorer

Theorem lfinun

Description: Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020)

Ref Expression
Assertion lfinun ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → A ∪ B ∈ LocFin ⁡ J

Proof

Step Hyp Ref Expression
1 locfintop ⊢ A ∈ LocFin ⁡ J → J ∈ Top
2 1 ad2antrr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → J ∈ Top
3 ssequn2 ⊢ ⋃ B ⊆ ⋃ J ↔ ⋃ J ∪ ⋃ B = ⋃ J
4 3 biimpi ⊢ ⋃ B ⊆ ⋃ J → ⋃ J ∪ ⋃ B = ⋃ J
5 4 adantl ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J ∪ ⋃ B = ⋃ J
6 eqid ⊢ ⋃ J = ⋃ J
7 eqid ⊢ ⋃ A = ⋃ A
8 6 7 locfinbas ⊢ A ∈ LocFin ⁡ J → ⋃ J = ⋃ A
9 8 ad2antrr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J = ⋃ A
10 9 uneq1d ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J ∪ ⋃ B = ⋃ A ∪ ⋃ B
11 5 10 eqtr3d ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J = ⋃ A ∪ ⋃ B
12 uniun ⊢ ⋃ A ∪ B = ⋃ A ∪ ⋃ B
13 11 12 eqtr4di ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J = ⋃ A ∪ B
14 6 locfinnei ⊢ A ∈ LocFin ⁡ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
15 14 ad4ant14 ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
16 simpr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A | s ∩ n ≠ ∅ ∈ Fin
17 rabfi ⊢ B ∈ Fin → s ∈ B | s ∩ n ≠ ∅ ∈ Fin
18 17 ad2antlr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ B | s ∩ n ≠ ∅ ∈ Fin
19 rabun2 ⊢ s ∈ A ∪ B | s ∩ n ≠ ∅ = s ∈ A | s ∩ n ≠ ∅ ∪ s ∈ B | s ∩ n ≠ ∅
20 unfi ⊢ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ∧ s ∈ B | s ∩ n ≠ ∅ ∈ Fin → s ∈ A | s ∩ n ≠ ∅ ∪ s ∈ B | s ∩ n ≠ ∅ ∈ Fin
21 19 20 eqeltrid ⊢ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ∧ s ∈ B | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
22 16 18 21 syl2anc ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
23 22 ex ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin → s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
24 23 ad2antrr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
25 24 anim2d ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
26 25 reximdv ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
27 15 26 mpd ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
28 27 ralrimiva ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ∀ x ∈ ⋃ J ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
29 2 13 28 3jca ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → J ∈ Top ∧ ⋃ J = ⋃ A ∪ B ∧ ∀ x ∈ ⋃ J ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
30 29 3impa ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → J ∈ Top ∧ ⋃ J = ⋃ A ∪ B ∧ ∀ x ∈ ⋃ J ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
31 eqid ⊢ ⋃ A ∪ B = ⋃ A ∪ B
32 6 31 islocfin ⊢ A ∪ B ∈ LocFin ⁡ J ↔ J ∈ Top ∧ ⋃ J = ⋃ A ∪ B ∧ ∀ x ∈ ⋃ J ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
33 30 32 sylibr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → A ∪ B ∈ LocFin ⁡ J