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