Proof of Theorem lmbrf
Step | Hyp | Ref
| Expression |
1 | | lmbr.2 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | lmbr2.4 |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | | lmbr2.5 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | 1, 2, 3 | lmbr2 20873 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
5 | | 3anass 1035 |
. . 3
⊢ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
(𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
6 | 2 | uztrn2 11581 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
7 | | lmbrf.7 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
8 | 7 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ 𝐴 ∈ 𝑢)) |
9 | | lmbrf.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) |
10 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑍⟶𝑋 → dom 𝐹 = 𝑍) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐹 = 𝑍) |
12 | 11 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ 𝑍)) |
13 | 12 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ dom 𝐹) |
14 | 13 | biantrurd 528 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
15 | 8, 14 | bitr3d 269 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴 ∈ 𝑢 ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
16 | 6, 15 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐴 ∈ 𝑢 ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
17 | 16 | anassrs 678 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐴 ∈ 𝑢 ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
18 | 17 | ralbidva 2968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
19 | 18 | rexbidva 3031 |
. . . . . . 7
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
20 | 19 | imbi2d 329 |
. . . . . 6
⊢ (𝜑 → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢) ↔ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
21 | 20 | ralbidv 2969 |
. . . . 5
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢) ↔ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
22 | 21 | anbi2d 736 |
. . . 4
⊢ (𝜑 → ((𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
23 | | toponmax 20543 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
24 | 1, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
25 | | cnex 9896 |
. . . . . . 7
⊢ ℂ
∈ V |
26 | 24, 25 | jctir 559 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐽 ∧ ℂ ∈ V)) |
27 | | uzssz 11583 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
28 | | zsscn 11262 |
. . . . . . . . 9
⊢ ℤ
⊆ ℂ |
29 | 27, 28 | sstri 3577 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ⊆ ℂ |
30 | 2, 29 | eqsstri 3598 |
. . . . . . 7
⊢ 𝑍 ⊆
ℂ |
31 | 9, 30 | jctir 559 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝑍⟶𝑋 ∧ 𝑍 ⊆ ℂ)) |
32 | | elpm2r 7761 |
. . . . . 6
⊢ (((𝑋 ∈ 𝐽 ∧ ℂ ∈ V) ∧ (𝐹:𝑍⟶𝑋 ∧ 𝑍 ⊆ ℂ)) → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
33 | 26, 31, 32 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
34 | 33 | biantrurd 528 |
. . . 4
⊢ (𝜑 → ((𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
(𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))))) |
35 | 22, 34 | bitr2d 268 |
. . 3
⊢ (𝜑 → ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
(𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)))) |
36 | 5, 35 | syl5bb 271 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)))) |
37 | 4, 36 | bitrd 267 |
1
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)))) |