Step | Hyp | Ref
| Expression |
1 | | uzf 11566 |
. . . . . . . 8
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
2 | | ffn 5958 |
. . . . . . . 8
⊢
(ℤ≥:ℤ⟶𝒫 ℤ →
ℤ≥ Fn ℤ) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢
ℤ≥ Fn ℤ |
4 | | lmflf.1 |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | | uzssz 11583 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
6 | 4, 5 | eqsstri 3598 |
. . . . . . 7
⊢ 𝑍 ⊆
ℤ |
7 | | imaeq2 5381 |
. . . . . . . . 9
⊢ (𝑦 =
(ℤ≥‘𝑗) → (𝐹 “ 𝑦) = (𝐹 “ (ℤ≥‘𝑗))) |
8 | 7 | sseq1d 3595 |
. . . . . . . 8
⊢ (𝑦 =
(ℤ≥‘𝑗) → ((𝐹 “ 𝑦) ⊆ 𝑥 ↔ (𝐹 “ (ℤ≥‘𝑗)) ⊆ 𝑥)) |
9 | 8 | rexima 6401 |
. . . . . . 7
⊢
((ℤ≥ Fn ℤ ∧ 𝑍 ⊆ ℤ) → (∃𝑦 ∈ (ℤ≥
“ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥 ↔ ∃𝑗 ∈ 𝑍 (𝐹 “ (ℤ≥‘𝑗)) ⊆ 𝑥)) |
10 | 3, 6, 9 | mp2an 704 |
. . . . . 6
⊢
(∃𝑦 ∈
(ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥 ↔ ∃𝑗 ∈ 𝑍 (𝐹 “ (ℤ≥‘𝑗)) ⊆ 𝑥) |
11 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → 𝐹:𝑍⟶𝑋) |
12 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐹:𝑍⟶𝑋 → Fun 𝐹) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → Fun 𝐹) |
14 | | uzss 11584 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑗) ⊆
(ℤ≥‘𝑀)) |
15 | 14, 4 | eleq2s 2706 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑍 → (ℤ≥‘𝑗) ⊆
(ℤ≥‘𝑀)) |
16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → (ℤ≥‘𝑗) ⊆
(ℤ≥‘𝑀)) |
17 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐹:𝑍⟶𝑋 → dom 𝐹 = 𝑍) |
18 | 11, 17 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → dom 𝐹 = 𝑍) |
19 | 18, 4 | syl6eq 2660 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → dom 𝐹 = (ℤ≥‘𝑀)) |
20 | 16, 19 | sseqtr4d 3605 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → (ℤ≥‘𝑗) ⊆ dom 𝐹) |
21 | | funimass4 6157 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧
(ℤ≥‘𝑗) ⊆ dom 𝐹) → ((𝐹 “ (ℤ≥‘𝑗)) ⊆ 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)) |
22 | 13, 20, 21 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑗 ∈ 𝑍) → ((𝐹 “ (ℤ≥‘𝑗)) ⊆ 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)) |
23 | 22 | rexbidva 3031 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (∃𝑗 ∈ 𝑍 (𝐹 “ (ℤ≥‘𝑗)) ⊆ 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)) |
24 | 10, 23 | syl5rbb 272 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ↔ ∃𝑦 ∈ (ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥)) |
25 | 24 | imbi2d 329 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → ((𝑃 ∈ 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥) ↔ (𝑃 ∈ 𝑥 → ∃𝑦 ∈ (ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥))) |
26 | 25 | ralbidv 2969 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑦 ∈ (ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥))) |
27 | 26 | anbi2d 736 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → ((𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑦 ∈ (ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥)))) |
28 | | simp1 1054 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
29 | | simp2 1055 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → 𝑀 ∈ ℤ) |
30 | | simp3 1056 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → 𝐹:𝑍⟶𝑋) |
31 | | eqidd 2611 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
32 | 28, 4, 29, 30, 31 | lmbrf 20874 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)))) |
33 | 4 | uzfbas 21512 |
. . 3
⊢ (𝑀 ∈ ℤ →
(ℤ≥ “ 𝑍) ∈ (fBas‘𝑍)) |
34 | | lmflf.2 |
. . . 4
⊢ 𝐿 = (𝑍filGen(ℤ≥ “ 𝑍)) |
35 | 34 | flffbas 21609 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (ℤ≥
“ 𝑍) ∈
(fBas‘𝑍) ∧ 𝐹:𝑍⟶𝑋) → (𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑦 ∈ (ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥)))) |
36 | 33, 35 | syl3an2 1352 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑦 ∈ (ℤ≥ “ 𝑍)(𝐹 “ 𝑦) ⊆ 𝑥)))) |
37 | 27, 32, 36 | 3bitr4d 299 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹))) |