| Step | Hyp | Ref
| Expression |
| 1 | | df-locfin 23515 |
. . . 4
⊢ LocFin =
(𝑗 ∈ Top ↦
{𝑦 ∣ (∪ 𝑗 =
∪ 𝑦 ∧ ∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
| 2 | 1 | mptrcl 7025 |
. . 3
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) |
| 3 | | eqimss2 4043 |
. . . . . . . . . . 11
⊢ (𝑋 = ∪
𝑦 → ∪ 𝑦
⊆ 𝑋) |
| 4 | | sspwuni 5100 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦
⊆ 𝑋) |
| 5 | 3, 4 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝑋 = ∪
𝑦 → 𝑦 ⊆ 𝒫 𝑋) |
| 6 | | velpw 4605 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 ↔ 𝑦 ⊆ 𝒫 𝑋) |
| 7 | 5, 6 | sylibr 234 |
. . . . . . . . 9
⊢ (𝑋 = ∪
𝑦 → 𝑦 ∈ 𝒫 𝒫 𝑋) |
| 8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝑋 = ∪
𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) → 𝑦 ∈ 𝒫 𝒫
𝑋) |
| 9 | 8 | abssi 4070 |
. . . . . . 7
⊢ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ⊆
𝒫 𝒫 𝑋 |
| 10 | | islocfin.1 |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
| 11 | 10 | topopn 22912 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
| 12 | | pwexg 5378 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V) |
| 13 | | pwexg 5378 |
. . . . . . . 8
⊢
(𝒫 𝑋 ∈
V → 𝒫 𝒫 𝑋 ∈ V) |
| 14 | 11, 12, 13 | 3syl 18 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝒫
𝒫 𝑋 ∈
V) |
| 15 | | ssexg 5323 |
. . . . . . 7
⊢ (({𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ⊆
𝒫 𝒫 𝑋 ∧
𝒫 𝒫 𝑋
∈ V) → {𝑦 ∣
(𝑋 = ∪ 𝑦
∧ ∀𝑥 ∈
𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ∈
V) |
| 16 | 9, 14, 15 | sylancr 587 |
. . . . . 6
⊢ (𝐽 ∈ Top → {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ∈
V) |
| 17 | | unieq 4918 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪
𝐽) |
| 18 | 17, 10 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = 𝑋) |
| 19 | 18 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (∪ 𝑗 = ∪
𝑦 ↔ 𝑋 = ∪ 𝑦)) |
| 20 | | rexeq 3322 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → (∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 21 | 18, 20 | raleqbidv 3346 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 22 | 19, 21 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ((∪ 𝑗 = ∪
𝑦 ∧ ∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) ↔ (𝑋 = ∪
𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 23 | 22 | abbidv 2808 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → {𝑦 ∣ (∪ 𝑗 = ∪
𝑦 ∧ ∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} = {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
| 24 | 23, 1 | fvmptg 7014 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ∈ V)
→ (LocFin‘𝐽) =
{𝑦 ∣ (𝑋 = ∪
𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
| 25 | 16, 24 | mpdan 687 |
. . . . 5
⊢ (𝐽 ∈ Top →
(LocFin‘𝐽) = {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
| 26 | 25 | eleq2d 2827 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐴 ∈ (LocFin‘𝐽) ↔ 𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))})) |
| 27 | | elex 3501 |
. . . . . 6
⊢ (𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} → 𝐴 ∈ V) |
| 28 | 27 | adantl 481 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))}) → 𝐴 ∈ V) |
| 29 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌) |
| 30 | | islocfin.2 |
. . . . . . . . . 10
⊢ 𝑌 = ∪
𝐴 |
| 31 | 29, 30 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝑋 = ∪ 𝐴) |
| 32 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝑋 ∈ 𝐽) |
| 33 | 31, 32 | eqeltrrd 2842 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → ∪ 𝐴 ∈ 𝐽) |
| 34 | 33 | elexd 3504 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → ∪ 𝐴 ∈ V) |
| 35 | | uniexb 7784 |
. . . . . . 7
⊢ (𝐴 ∈ V ↔ ∪ 𝐴
∈ V) |
| 36 | 34, 35 | sylibr 234 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝐴 ∈ V) |
| 37 | 36 | adantrr 717 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))) → 𝐴 ∈ V) |
| 38 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∪ 𝑦 = ∪
𝐴) |
| 39 | 38, 30 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ∪ 𝑦 = 𝑌) |
| 40 | 39 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = 𝑌)) |
| 41 | | rabeq 3451 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} = {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → ({𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ↔ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
| 43 | 42 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔ (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 44 | 43 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 45 | 44 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
| 46 | 40, 45 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 47 | 46 | elabg 3676 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 48 | 28, 37, 47 | pm5.21nd 802 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 49 | 26, 48 | bitrd 279 |
. . 3
⊢ (𝐽 ∈ Top → (𝐴 ∈ (LocFin‘𝐽) ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 50 | 2, 49 | biadanii 822 |
. 2
⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 51 | | 3anass 1095 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) ↔ (𝐽 ∈ Top ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
| 52 | 50, 51 | bitr4i 278 |
1
⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |