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 ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ( 𝐴 ∪ 𝐵 ) ∈ ( LocFin ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 locfintop ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝐽 ∈ Top )
2 1 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → 𝐽 ∈ Top )
3 ssequn2 ⊢ ( ∪ 𝐵 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∪ ∪ 𝐵 ) = ∪ 𝐽 )
4 3 biimpi ⊢ ( ∪ 𝐵 ⊆ ∪ 𝐽 → ( ∪ 𝐽 ∪ ∪ 𝐵 ) = ∪ 𝐽 )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ( ∪ 𝐽 ∪ ∪ 𝐵 ) = ∪ 𝐽 )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
8 6 7 locfinbas ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → ∪ 𝐽 = ∪ 𝐴 )
9 8 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ∪ 𝐽 = ∪ 𝐴 )
10 9 uneq1d ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ( ∪ 𝐽 ∪ ∪ 𝐵 ) = ( ∪ 𝐴 ∪ ∪ 𝐵 ) )
11 5 10 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ∪ 𝐽 = ( ∪ 𝐴 ∪ ∪ 𝐵 ) )
12 uniun ⊢ ∪ ( 𝐴 ∪ 𝐵 ) = ( ∪ 𝐴 ∪ ∪ 𝐵 )
13 11 12 eqtr4di ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ∪ 𝐽 = ∪ ( 𝐴 ∪ 𝐵 ) )
14 6 locfinnei ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
15 14 ad4ant14 ⊢ ( ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
16 simpr ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
17 rabfi ⊢ ( 𝐵 ∈ Fin → { 𝑠 ∈ 𝐵 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
18 17 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → { 𝑠 ∈ 𝐵 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
19 rabun2 ⊢ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } = ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∪ { 𝑠 ∈ 𝐵 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } )
20 unfi ⊢ ( ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ∧ { 𝑠 ∈ 𝐵 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∪ { 𝑠 ∈ 𝐵 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ) ∈ Fin )
21 19 20 eqeltrid ⊢ ( ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ∧ { 𝑠 ∈ 𝐵 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
22 16 18 21 syl2anc ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
23 22 ex ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) → ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin → { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
24 23 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin → { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
25 24 anim2d ⊢ ( ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
26 25 reximdv ⊢ ( ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
27 15 26 mpd ⊢ ( ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
28 27 ralrimiva ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
29 2 13 28 3jca ⊢ ( ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ) ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ( 𝐽 ∈ Top ∧ ∪ 𝐽 = ∪ ( 𝐴 ∪ 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
30 29 3impa ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ( 𝐽 ∈ Top ∧ ∪ 𝐽 = ∪ ( 𝐴 ∪ 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
31 eqid ⊢ ∪ ( 𝐴 ∪ 𝐵 ) = ∪ ( 𝐴 ∪ 𝐵 )
32 6 31 islocfin ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ ∪ 𝐽 = ∪ ( 𝐴 ∪ 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
33 30 32 sylibr ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵 ⊆ ∪ 𝐽 ) → ( 𝐴 ∪ 𝐵 ) ∈ ( LocFin ‘ 𝐽 ) )