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∈Jx∈n∧s∈A|s∩n≠∅∈Fin
15 14 ad4ant14 ⊢A∈LocFin⁡J∧B∈Fin∧⋃B⊆⋃J∧x∈⋃J→∃n∈Jx∈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∈Jx∈n∧s∈A|s∩n≠∅∈Fin→∃n∈Jx∈n∧s∈A∪B|s∩n≠∅∈Fin
27 15 26 mpd ⊢A∈LocFin⁡J∧B∈Fin∧⋃B⊆⋃J∧x∈⋃J→∃n∈Jx∈n∧s∈A∪B|s∩n≠∅∈Fin
28 27 ralrimiva ⊢A∈LocFin⁡J∧B∈Fin∧⋃B⊆⋃J→∀x∈⋃J∃n∈Jx∈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∈Jx∈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∈Jx∈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∈Jx∈n∧s∈A∪B|s∩n≠∅∈Fin
33 30 32 sylibr ⊢A∈LocFin⁡J∧B∈Fin∧⋃B⊆⋃J→A∪B∈LocFin⁡J