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 bilani ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J ∪ ⋃ B = ⋃ J
5 eqid ⊢ ⋃ J = ⋃ J
6 eqid ⊢ ⋃ A = ⋃ A
7 5 6 locfinbas ⊢ A ∈ LocFin ⁡ J → ⋃ J = ⋃ A
8 7 ad2antrr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J = ⋃ A
9 8 uneq1d ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J ∪ ⋃ B = ⋃ A ∪ ⋃ B
10 4 9 eqtr3d ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J = ⋃ A ∪ ⋃ B
11 uniun ⊢ ⋃ A ∪ B = ⋃ A ∪ ⋃ B
12 10 11 eqtr4di ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ⋃ J = ⋃ A ∪ B
13 5 locfinnei ⊢ A ∈ LocFin ⁡ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
14 13 ad4ant14 ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
15 simpr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A | s ∩ n ≠ ∅ ∈ Fin
16 rabfi ⊢ B ∈ Fin → s ∈ B | s ∩ n ≠ ∅ ∈ Fin
17 16 ad2antlr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ B | s ∩ n ≠ ∅ ∈ Fin
18 rabun2 ⊢ s ∈ A ∪ B | s ∩ n ≠ ∅ = s ∈ A | s ∩ n ≠ ∅ ∪ s ∈ B | s ∩ n ≠ ∅
19 unfi ⊢ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ∧ s ∈ B | s ∩ n ≠ ∅ ∈ Fin → s ∈ A | s ∩ n ≠ ∅ ∪ s ∈ B | s ∩ n ≠ ∅ ∈ Fin
20 18 19 eqeltrid ⊢ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ∧ s ∈ B | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
21 15 17 20 syl2anc ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
22 21 ex ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin → s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
23 22 ad2antrr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → s ∈ A | s ∩ n ≠ ∅ ∈ Fin → s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
24 23 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
25 24 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
26 14 25 mpd ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J ∧ x ∈ ⋃ J → ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
27 26 ralrimiva ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → ∀ x ∈ ⋃ J ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
28 2 12 27 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
29 28 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
30 eqid ⊢ ⋃ A ∪ B = ⋃ A ∪ B
31 5 30 islocfin ⊢ A ∪ B ∈ LocFin ⁡ J ↔ J ∈ Top ∧ ⋃ J = ⋃ A ∪ B ∧ ∀ x ∈ ⋃ J ∃ n ∈ J x ∈ n ∧ s ∈ A ∪ B | s ∩ n ≠ ∅ ∈ Fin
32 29 31 sylibr ⊢ A ∈ LocFin ⁡ J ∧ B ∈ Fin ∧ ⋃ B ⊆ ⋃ J → A ∪ B ∈ LocFin ⁡ J