| Step | Hyp | Ref
| Expression |
| 1 | | lmbr3.2 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 2 | 1 | lmbr3v 45760 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → ∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣))))) |
| 3 | | eleq2w 2825 |
. . . . 5
⊢ (𝑣 = 𝑢 → (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ 𝑢)) |
| 4 | | eleq2w 2825 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → ((𝐹‘𝑙) ∈ 𝑣 ↔ (𝐹‘𝑙) ∈ 𝑢)) |
| 5 | 4 | anbi2d 630 |
. . . . . . 7
⊢ (𝑣 = 𝑢 → ((𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣) ↔ (𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢))) |
| 6 | 5 | rexralbidv 3223 |
. . . . . 6
⊢ (𝑣 = 𝑢 → (∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣) ↔ ∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢))) |
| 7 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (ℤ≥‘𝑖) =
(ℤ≥‘𝑗)) |
| 8 | 7 | raleqdv 3326 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢) ↔ ∀𝑙 ∈ (ℤ≥‘𝑗)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢))) |
| 9 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑙 |
| 10 | | lmbr3.1 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝐹 |
| 11 | 10 | nfdm 5962 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘dom
𝐹 |
| 12 | 9, 11 | nfel 2920 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑙 ∈ dom 𝐹 |
| 13 | 10, 9 | nffv 6916 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐹‘𝑙) |
| 14 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑢 |
| 15 | 13, 14 | nfel 2920 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝐹‘𝑙) ∈ 𝑢 |
| 16 | 12, 15 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢) |
| 17 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑙(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) |
| 18 | | eleq1w 2824 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (𝑙 ∈ dom 𝐹 ↔ 𝑘 ∈ dom 𝐹)) |
| 19 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → (𝐹‘𝑙) = (𝐹‘𝑘)) |
| 20 | 19 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → ((𝐹‘𝑙) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ 𝑢)) |
| 21 | 18, 20 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑙 = 𝑘 → ((𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 22 | 16, 17, 21 | cbvralw 3306 |
. . . . . . . 8
⊢
(∀𝑙 ∈
(ℤ≥‘𝑗)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 23 | 8, 22 | bitrdi 287 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 24 | 23 | cbvrexvw 3238 |
. . . . . 6
⊢
(∃𝑖 ∈
ℤ ∀𝑙 ∈
(ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 25 | 6, 24 | bitrdi 287 |
. . . . 5
⊢ (𝑣 = 𝑢 → (∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 26 | 3, 25 | imbi12d 344 |
. . . 4
⊢ (𝑣 = 𝑢 → ((𝑃 ∈ 𝑣 → ∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣)) ↔ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 27 | 26 | cbvralvw 3237 |
. . 3
⊢
(∀𝑣 ∈
𝐽 (𝑃 ∈ 𝑣 → ∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣)) ↔ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 28 | 27 | 3anbi3i 1160 |
. 2
⊢ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → ∃𝑖 ∈ ℤ ∀𝑙 ∈ (ℤ≥‘𝑖)(𝑙 ∈ dom 𝐹 ∧ (𝐹‘𝑙) ∈ 𝑣))) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 29 | 2, 28 | bitrdi 287 |
1
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |