Step | Hyp | Ref
| Expression |
1 | | locfintop 21134 |
. . . . 5
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) |
2 | 1 | ad2antrr 758 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → 𝐽 ∈ Top) |
3 | | ssequn2 3748 |
. . . . . . . 8
⊢ (∪ 𝐵
⊆ ∪ 𝐽 ↔ (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
4 | 3 | biimpi 205 |
. . . . . . 7
⊢ (∪ 𝐵
⊆ ∪ 𝐽 → (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
6 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
7 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐴 =
∪ 𝐴 |
8 | 6, 7 | locfinbas 21135 |
. . . . . . . 8
⊢ (𝐴 ∈ (LocFin‘𝐽) → ∪ 𝐽 =
∪ 𝐴) |
9 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = ∪
𝐴) |
10 | 9 | uneq1d 3728 |
. . . . . 6
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (∪ 𝐽 ∪ ∪ 𝐵) =
(∪ 𝐴 ∪ ∪ 𝐵)) |
11 | 5, 10 | eqtr3d 2646 |
. . . . 5
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = (∪
𝐴 ∪ ∪ 𝐵)) |
12 | | uniun 4392 |
. . . . 5
⊢ ∪ (𝐴
∪ 𝐵) = (∪ 𝐴
∪ ∪ 𝐵) |
13 | 11, 12 | syl6eqr 2662 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = ∪
(𝐴 ∪ 𝐵)) |
14 | 6 | locfinnei 21136 |
. . . . . . . 8
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
15 | 14 | adantlr 747 |
. . . . . . 7
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
16 | 15 | adantlr 747 |
. . . . . 6
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
17 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
18 | | rabfi 8070 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Fin → {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
19 | 18 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
20 | | rabun2 3865 |
. . . . . . . . . . . 12
⊢ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} = ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∪ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) |
21 | | unfi 8112 |
. . . . . . . . . . . 12
⊢ (({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ∧ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∪ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) ∈ Fin) |
22 | 20, 21 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ∧ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
23 | 17, 19, 22 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
24 | 23 | ex 449 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
25 | 24 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
26 | 25 | anim2d 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ((𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
27 | 26 | reximdv 2999 |
. . . . . 6
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → (∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
28 | 16, 27 | mpd 15 |
. . . . 5
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
29 | 28 | ralrimiva 2949 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
30 | 2, 13, 29 | 3jca 1235 |
. . 3
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
31 | 30 | 3impa 1251 |
. 2
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
32 | | eqid 2610 |
. . 3
⊢ ∪ (𝐴
∪ 𝐵) = ∪ (𝐴
∪ 𝐵) |
33 | 6, 32 | islocfin 21130 |
. 2
⊢ ((𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
34 | 31, 33 | sylibr 223 |
1
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽)) |