Step | Hyp | Ref
| Expression |
1 | | locfintop 21324 |
. . . . 5
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) |
2 | 1 | ad2antrr 762 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → 𝐽 ∈ Top) |
3 | | ssequn2 3786 |
. . . . . . . 8
⊢ (∪ 𝐵
⊆ ∪ 𝐽 ↔ (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
4 | 3 | biimpi 206 |
. . . . . . 7
⊢ (∪ 𝐵
⊆ ∪ 𝐽 → (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
5 | 4 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
6 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
7 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ 𝐴 =
∪ 𝐴 |
8 | 6, 7 | locfinbas 21325 |
. . . . . . . 8
⊢ (𝐴 ∈ (LocFin‘𝐽) → ∪ 𝐽 =
∪ 𝐴) |
9 | 8 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = ∪
𝐴) |
10 | 9 | uneq1d 3766 |
. . . . . 6
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (∪ 𝐽 ∪ ∪ 𝐵) =
(∪ 𝐴 ∪ ∪ 𝐵)) |
11 | 5, 10 | eqtr3d 2658 |
. . . . 5
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = (∪
𝐴 ∪ ∪ 𝐵)) |
12 | | uniun 4456 |
. . . . 5
⊢ ∪ (𝐴
∪ 𝐵) = (∪ 𝐴
∪ ∪ 𝐵) |
13 | 11, 12 | syl6eqr 2674 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = ∪
(𝐴 ∪ 𝐵)) |
14 | 6 | locfinnei 21326 |
. . . . . . . 8
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
15 | 14 | adantlr 751 |
. . . . . . 7
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
16 | 15 | adantlr 751 |
. . . . . 6
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
17 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
18 | | rabfi 8185 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Fin → {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
19 | 18 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
20 | | rabun2 3906 |
. . . . . . . . . . . 12
⊢ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} = ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∪ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) |
21 | | unfi 8227 |
. . . . . . . . . . . 12
⊢ (({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ∧ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∪ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) ∈ Fin) |
22 | 20, 21 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ∧ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
23 | 17, 19, 22 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
24 | 23 | ex 450 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
25 | 24 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
26 | 25 | anim2d 589 |
. . . . . . 7
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ((𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
27 | 26 | reximdv 3016 |
. . . . . 6
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → (∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
28 | 16, 27 | mpd 15 |
. . . . 5
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
29 | 28 | ralrimiva 2966 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
30 | 2, 13, 29 | 3jca 1242 |
. . 3
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
31 | 30 | 3impa 1259 |
. 2
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
32 | | eqid 2622 |
. . 3
⊢ ∪ (𝐴
∪ 𝐵) = ∪ (𝐴
∪ 𝐵) |
33 | 6, 32 | islocfin 21320 |
. 2
⊢ ((𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
34 | 31, 33 | sylibr 224 |
1
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽)) |