| Step | Hyp | Ref
| Expression |
| 1 | | locfintop 23529 |
. . . . 5
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) |
| 2 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → 𝐽 ∈ Top) |
| 3 | | ssequn2 4189 |
. . . . . . . 8
⊢ (∪ 𝐵
⊆ ∪ 𝐽 ↔ (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
| 4 | 3 | biimpi 216 |
. . . . . . 7
⊢ (∪ 𝐵
⊆ ∪ 𝐽 → (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (∪ 𝐽 ∪ ∪ 𝐵) =
∪ 𝐽) |
| 6 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 7 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐴 =
∪ 𝐴 |
| 8 | 6, 7 | locfinbas 23530 |
. . . . . . . 8
⊢ (𝐴 ∈ (LocFin‘𝐽) → ∪ 𝐽 =
∪ 𝐴) |
| 9 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = ∪
𝐴) |
| 10 | 9 | uneq1d 4167 |
. . . . . 6
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (∪ 𝐽 ∪ ∪ 𝐵) =
(∪ 𝐴 ∪ ∪ 𝐵)) |
| 11 | 5, 10 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = (∪
𝐴 ∪ ∪ 𝐵)) |
| 12 | | uniun 4930 |
. . . . 5
⊢ ∪ (𝐴
∪ 𝐵) = (∪ 𝐴
∪ ∪ 𝐵) |
| 13 | 11, 12 | eqtr4di 2795 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∪ 𝐽 = ∪
(𝐴 ∪ 𝐵)) |
| 14 | 6 | locfinnei 23531 |
. . . . . . 7
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 15 | 14 | ad4ant14 752 |
. . . . . 6
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 16 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
| 17 | | rabfi 9303 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Fin → {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
| 18 | 17 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
| 19 | | rabun2 4324 |
. . . . . . . . . . . 12
⊢ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} = ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∪ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) |
| 20 | | unfi 9211 |
. . . . . . . . . . . 12
⊢ (({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ∧ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∪ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) ∈ Fin) |
| 21 | 19, 20 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ∧ {𝑠 ∈ 𝐵 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
| 22 | 16, 18, 21 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) |
| 23 | 22 | ex 412 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ({𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin → {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 25 | 24 | anim2d 612 |
. . . . . . 7
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ((𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 26 | 25 | reximdv 3170 |
. . . . . 6
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → (∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 27 | 15, 26 | mpd 15 |
. . . . 5
⊢ ((((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 28 | 27 | ralrimiva 3146 |
. . . 4
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 29 | 2, 13, 28 | 3jca 1129 |
. . 3
⊢ (((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin) ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 30 | 29 | 3impa 1110 |
. 2
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 31 | | eqid 2737 |
. . 3
⊢ ∪ (𝐴
∪ 𝐵) = ∪ (𝐴
∪ 𝐵) |
| 32 | 6, 31 | islocfin 23525 |
. 2
⊢ ((𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ ∪ 𝐽 =
∪ (𝐴 ∪ 𝐵) ∧ ∀𝑥 ∈ ∪ 𝐽∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ (𝐴 ∪ 𝐵) ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 33 | 30, 32 | sylibr 234 |
1
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵
⊆ ∪ 𝐽) → (𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽)) |