Step | Hyp | Ref
| Expression |
1 | | df-locfin 21120 |
. . . . 5
⊢ LocFin =
(𝑗 ∈ Top ↦
{𝑦 ∣ (∪ 𝑗 =
∪ 𝑦 ∧ ∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
2 | 1 | dmmptss 5548 |
. . . 4
⊢ dom
LocFin ⊆ Top |
3 | | elfvdm 6130 |
. . . 4
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ dom LocFin) |
4 | 2, 3 | sseldi 3566 |
. . 3
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) |
5 | | eqimss2 3621 |
. . . . . . . . . . 11
⊢ (𝑋 = ∪
𝑦 → ∪ 𝑦
⊆ 𝑋) |
6 | | sspwuni 4547 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦
⊆ 𝑋) |
7 | 5, 6 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝑋 = ∪
𝑦 → 𝑦 ⊆ 𝒫 𝑋) |
8 | | selpw 4115 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 ↔ 𝑦 ⊆ 𝒫 𝑋) |
9 | 7, 8 | sylibr 223 |
. . . . . . . . 9
⊢ (𝑋 = ∪
𝑦 → 𝑦 ∈ 𝒫 𝒫 𝑋) |
10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝑋 = ∪
𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) → 𝑦 ∈ 𝒫 𝒫
𝑋) |
11 | 10 | abssi 3640 |
. . . . . . 7
⊢ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ⊆
𝒫 𝒫 𝑋 |
12 | | islocfin.1 |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
13 | 12 | topopn 20536 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
14 | | pwexg 4776 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V) |
15 | | pwexg 4776 |
. . . . . . . 8
⊢
(𝒫 𝑋 ∈
V → 𝒫 𝒫 𝑋 ∈ V) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝒫
𝒫 𝑋 ∈
V) |
17 | | ssexg 4732 |
. . . . . . 7
⊢ (({𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ⊆
𝒫 𝒫 𝑋 ∧
𝒫 𝒫 𝑋
∈ V) → {𝑦 ∣
(𝑋 = ∪ 𝑦
∧ ∀𝑥 ∈
𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ∈
V) |
18 | 11, 16, 17 | sylancr 694 |
. . . . . 6
⊢ (𝐽 ∈ Top → {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ∈
V) |
19 | | unieq 4380 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪
𝐽) |
20 | 19, 12 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = 𝑋) |
21 | 20 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (∪ 𝑗 = ∪
𝑦 ↔ 𝑋 = ∪ 𝑦)) |
22 | | rexeq 3116 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → (∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
23 | 20, 22 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
24 | 21, 23 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ((∪ 𝑗 = ∪
𝑦 ∧ ∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) ↔ (𝑋 = ∪
𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
25 | 24 | abbidv 2728 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → {𝑦 ∣ (∪ 𝑗 = ∪
𝑦 ∧ ∀𝑥 ∈ ∪ 𝑗∃𝑛 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} = {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
26 | 25, 1 | fvmptg 6189 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ∈ V)
→ (LocFin‘𝐽) =
{𝑦 ∣ (𝑋 = ∪
𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
27 | 18, 26 | mpdan 699 |
. . . . 5
⊢ (𝐽 ∈ Top →
(LocFin‘𝐽) = {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))}) |
28 | 27 | eleq2d 2673 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐴 ∈ (LocFin‘𝐽) ↔ 𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))})) |
29 | | elex 3185 |
. . . . . 6
⊢ (𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} → 𝐴 ∈ V) |
30 | 29 | adantl 481 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))}) → 𝐴 ∈ V) |
31 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌) |
32 | | islocfin.2 |
. . . . . . . . . 10
⊢ 𝑌 = ∪
𝐴 |
33 | 31, 32 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝑋 = ∪ 𝐴) |
34 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝑋 ∈ 𝐽) |
35 | 33, 34 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → ∪ 𝐴 ∈ 𝐽) |
36 | | elex 3185 |
. . . . . . . 8
⊢ (∪ 𝐴
∈ 𝐽 → ∪ 𝐴
∈ V) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → ∪ 𝐴 ∈ V) |
38 | | uniexb 6866 |
. . . . . . 7
⊢ (𝐴 ∈ V ↔ ∪ 𝐴
∈ V) |
39 | 37, 38 | sylibr 223 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌) → 𝐴 ∈ V) |
40 | 39 | adantrr 749 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))) → 𝐴 ∈ V) |
41 | | unieq 4380 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∪ 𝑦 = ∪
𝐴) |
42 | 41, 32 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ∪ 𝑦 = 𝑌) |
43 | 42 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = 𝑌)) |
44 | | rabeq 3166 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} = {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅}) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → ({𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin ↔ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
46 | 45 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔ (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
47 | 46 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
48 | 47 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) ↔
∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
49 | 43, 48 | anbi12d 743 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
50 | 49 | elabg 3320 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
51 | 30, 40, 50 | pm5.21nd 939 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐴 ∈ {𝑦 ∣ (𝑋 = ∪ 𝑦 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))} ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
52 | 28, 51 | bitrd 267 |
. . 3
⊢ (𝐽 ∈ Top → (𝐴 ∈ (LocFin‘𝐽) ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
53 | 4, 52 | biadan2 672 |
. 2
⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
54 | | 3anass 1035 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) ↔ (𝐽 ∈ Top ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin)))) |
55 | 53, 54 | bitr4i 266 |
1
⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |