Step | Hyp | Ref
| Expression |
1 | | rfcnpre4.2 |
. . . . . . . 8
⊢ 𝐾 = (topGen‘ran
(,)) |
2 | | rfcnpre4.3 |
. . . . . . . 8
⊢ 𝑇 = ∪
𝐽 |
3 | | eqid 2738 |
. . . . . . . 8
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾) |
4 | | rfcnpre4.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
5 | 1, 2, 3, 4 | fcnre 42256 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
6 | | ffn 6554 |
. . . . . . 7
⊢ (𝐹:𝑇⟶ℝ → 𝐹 Fn 𝑇) |
7 | | elpreima 6887 |
. . . . . . 7
⊢ (𝐹 Fn 𝑇 → (𝑠 ∈ (◡𝐹 “ (-∞(,]𝐵)) ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ∈ (-∞(,]𝐵)))) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (◡𝐹 “ (-∞(,]𝐵)) ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ∈ (-∞(,]𝐵)))) |
9 | | mnfxr 10903 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
10 | | rfcnpre4.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
11 | 10 | rexrd 10896 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
12 | 11 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝐵 ∈
ℝ*) |
13 | | elioc1 12990 |
. . . . . . . . 9
⊢
((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐹‘𝑠) ∈ (-∞(,]𝐵) ↔ ((𝐹‘𝑠) ∈ ℝ* ∧ -∞
< (𝐹‘𝑠) ∧ (𝐹‘𝑠) ≤ 𝐵))) |
14 | 9, 12, 13 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → ((𝐹‘𝑠) ∈ (-∞(,]𝐵) ↔ ((𝐹‘𝑠) ∈ ℝ* ∧ -∞
< (𝐹‘𝑠) ∧ (𝐹‘𝑠) ≤ 𝐵))) |
15 | | simpr3 1198 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ ((𝐹‘𝑠) ∈ ℝ* ∧ -∞
< (𝐹‘𝑠) ∧ (𝐹‘𝑠) ≤ 𝐵)) → (𝐹‘𝑠) ≤ 𝐵) |
16 | 5 | ffvelrnda 6913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈ ℝ) |
17 | 16 | rexrd 10896 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈
ℝ*) |
18 | 17 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝐹‘𝑠) ≤ 𝐵) → (𝐹‘𝑠) ∈
ℝ*) |
19 | 16 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝐹‘𝑠) ≤ 𝐵) → (𝐹‘𝑠) ∈ ℝ) |
20 | | mnflt 12728 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑠) ∈ ℝ → -∞ < (𝐹‘𝑠)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝐹‘𝑠) ≤ 𝐵) → -∞ < (𝐹‘𝑠)) |
22 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝐹‘𝑠) ≤ 𝐵) → (𝐹‘𝑠) ≤ 𝐵) |
23 | 18, 21, 22 | 3jca 1130 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝐹‘𝑠) ≤ 𝐵) → ((𝐹‘𝑠) ∈ ℝ* ∧ -∞
< (𝐹‘𝑠) ∧ (𝐹‘𝑠) ≤ 𝐵)) |
24 | 15, 23 | impbida 801 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (((𝐹‘𝑠) ∈ ℝ* ∧ -∞
< (𝐹‘𝑠) ∧ (𝐹‘𝑠) ≤ 𝐵) ↔ (𝐹‘𝑠) ≤ 𝐵)) |
25 | 14, 24 | bitrd 282 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → ((𝐹‘𝑠) ∈ (-∞(,]𝐵) ↔ (𝐹‘𝑠) ≤ 𝐵)) |
26 | 25 | pm5.32da 582 |
. . . . . 6
⊢ (𝜑 → ((𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ∈ (-∞(,]𝐵)) ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ≤ 𝐵))) |
27 | 8, 26 | bitrd 282 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (◡𝐹 “ (-∞(,]𝐵)) ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ≤ 𝐵))) |
28 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡𝑠 |
29 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡𝑇 |
30 | | rfcnpre4.1 |
. . . . . . . 8
⊢
Ⅎ𝑡𝐹 |
31 | 30, 28 | nffv 6736 |
. . . . . . 7
⊢
Ⅎ𝑡(𝐹‘𝑠) |
32 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑡
≤ |
33 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑡𝐵 |
34 | 31, 32, 33 | nfbr 5109 |
. . . . . 6
⊢
Ⅎ𝑡(𝐹‘𝑠) ≤ 𝐵 |
35 | | fveq2 6726 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (𝐹‘𝑡) = (𝐹‘𝑠)) |
36 | 35 | breq1d 5072 |
. . . . . 6
⊢ (𝑡 = 𝑠 → ((𝐹‘𝑡) ≤ 𝐵 ↔ (𝐹‘𝑠) ≤ 𝐵)) |
37 | 28, 29, 34, 36 | elrabf 3605 |
. . . . 5
⊢ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵} ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ≤ 𝐵)) |
38 | 27, 37 | bitr4di 292 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (◡𝐹 “ (-∞(,]𝐵)) ↔ 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵})) |
39 | 38 | eqrdv 2736 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵}) |
40 | | rfcnpre4.4 |
. . 3
⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵} |
41 | 39, 40 | eqtr4di 2797 |
. 2
⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) = 𝐴) |
42 | | iocmnfcld 23679 |
. . . . 5
⊢ (𝐵 ∈ ℝ →
(-∞(,]𝐵) ∈
(Clsd‘(topGen‘ran (,)))) |
43 | 10, 42 | syl 17 |
. . . 4
⊢ (𝜑 → (-∞(,]𝐵) ∈
(Clsd‘(topGen‘ran (,)))) |
44 | 1 | fveq2i 6729 |
. . . 4
⊢
(Clsd‘𝐾) =
(Clsd‘(topGen‘ran (,))) |
45 | 43, 44 | eleqtrrdi 2850 |
. . 3
⊢ (𝜑 → (-∞(,]𝐵) ∈ (Clsd‘𝐾)) |
46 | | cnclima 22178 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (-∞(,]𝐵) ∈ (Clsd‘𝐾)) → (◡𝐹 “ (-∞(,]𝐵)) ∈ (Clsd‘𝐽)) |
47 | 4, 45, 46 | syl2anc 587 |
. 2
⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) ∈ (Clsd‘𝐽)) |
48 | 41, 47 | eqeltrrd 2840 |
1
⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) |