| Step | Hyp | Ref
| Expression |
| 1 | | rfcnpre3.3 |
. . . . . . . 8
⊢ 𝐾 = (topGen‘ran
(,)) |
| 2 | | rfcnpre3.4 |
. . . . . . . 8
⊢ 𝑇 = ∪
𝐽 |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾) |
| 4 | | rfcnpre3.8 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 5 | 1, 2, 3, 4 | fcnre 45030 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
| 6 | | ffn 6736 |
. . . . . . 7
⊢ (𝐹:𝑇⟶ℝ → 𝐹 Fn 𝑇) |
| 7 | | elpreima 7078 |
. . . . . . 7
⊢ (𝐹 Fn 𝑇 → (𝑠 ∈ (◡𝐹 “ (𝐵[,)+∞)) ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ∈ (𝐵[,)+∞)))) |
| 8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (◡𝐹 “ (𝐵[,)+∞)) ↔ (𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ∈ (𝐵[,)+∞)))) |
| 9 | | rfcnpre3.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 10 | 9 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝐵 ∈
ℝ*) |
| 12 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 13 | | elico1 13430 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐹‘𝑠) ∈ (𝐵[,)+∞) ↔ ((𝐹‘𝑠) ∈ ℝ* ∧ 𝐵 ≤ (𝐹‘𝑠) ∧ (𝐹‘𝑠) < +∞))) |
| 14 | 11, 12, 13 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → ((𝐹‘𝑠) ∈ (𝐵[,)+∞) ↔ ((𝐹‘𝑠) ∈ ℝ* ∧ 𝐵 ≤ (𝐹‘𝑠) ∧ (𝐹‘𝑠) < +∞))) |
| 15 | | simpr2 1196 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ ((𝐹‘𝑠) ∈ ℝ* ∧ 𝐵 ≤ (𝐹‘𝑠) ∧ (𝐹‘𝑠) < +∞)) → 𝐵 ≤ (𝐹‘𝑠)) |
| 16 | 5 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈ ℝ) |
| 17 | 16 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈
ℝ*) |
| 18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ 𝐵 ≤ (𝐹‘𝑠)) → (𝐹‘𝑠) ∈
ℝ*) |
| 19 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ 𝐵 ≤ (𝐹‘𝑠)) → 𝐵 ≤ (𝐹‘𝑠)) |
| 20 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ 𝐵 ≤ (𝐹‘𝑠)) → (𝐹‘𝑠) ∈ ℝ) |
| 21 | | ltpnf 13162 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑠) ∈ ℝ → (𝐹‘𝑠) < +∞) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ 𝐵 ≤ (𝐹‘𝑠)) → (𝐹‘𝑠) < +∞) |
| 23 | 18, 19, 22 | 3jca 1129 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ 𝐵 ≤ (𝐹‘𝑠)) → ((𝐹‘𝑠) ∈ ℝ* ∧ 𝐵 ≤ (𝐹‘𝑠) ∧ (𝐹‘𝑠) < +∞)) |
| 24 | 15, 23 | impbida 801 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (((𝐹‘𝑠) ∈ ℝ* ∧ 𝐵 ≤ (𝐹‘𝑠) ∧ (𝐹‘𝑠) < +∞) ↔ 𝐵 ≤ (𝐹‘𝑠))) |
| 25 | 14, 24 | bitrd 279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → ((𝐹‘𝑠) ∈ (𝐵[,)+∞) ↔ 𝐵 ≤ (𝐹‘𝑠))) |
| 26 | 25 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → ((𝑠 ∈ 𝑇 ∧ (𝐹‘𝑠) ∈ (𝐵[,)+∞)) ↔ (𝑠 ∈ 𝑇 ∧ 𝐵 ≤ (𝐹‘𝑠)))) |
| 27 | 8, 26 | bitrd 279 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (◡𝐹 “ (𝐵[,)+∞)) ↔ (𝑠 ∈ 𝑇 ∧ 𝐵 ≤ (𝐹‘𝑠)))) |
| 28 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡𝑠 |
| 29 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡𝑇 |
| 30 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑡𝐵 |
| 31 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑡
≤ |
| 32 | | rfcnpre3.2 |
. . . . . . . 8
⊢
Ⅎ𝑡𝐹 |
| 33 | 32, 28 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑡(𝐹‘𝑠) |
| 34 | 30, 31, 33 | nfbr 5190 |
. . . . . 6
⊢
Ⅎ𝑡 𝐵 ≤ (𝐹‘𝑠) |
| 35 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (𝐹‘𝑡) = (𝐹‘𝑠)) |
| 36 | 35 | breq2d 5155 |
. . . . . 6
⊢ (𝑡 = 𝑠 → (𝐵 ≤ (𝐹‘𝑡) ↔ 𝐵 ≤ (𝐹‘𝑠))) |
| 37 | 28, 29, 34, 36 | elrabf 3688 |
. . . . 5
⊢ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)} ↔ (𝑠 ∈ 𝑇 ∧ 𝐵 ≤ (𝐹‘𝑠))) |
| 38 | 27, 37 | bitr4di 289 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (◡𝐹 “ (𝐵[,)+∞)) ↔ 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)})) |
| 39 | 38 | eqrdv 2735 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (𝐵[,)+∞)) = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)}) |
| 40 | | rfcnpre3.5 |
. . 3
⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)} |
| 41 | 39, 40 | eqtr4di 2795 |
. 2
⊢ (𝜑 → (◡𝐹 “ (𝐵[,)+∞)) = 𝐴) |
| 42 | | icopnfcld 24788 |
. . . . 5
⊢ (𝐵 ∈ ℝ → (𝐵[,)+∞) ∈
(Clsd‘(topGen‘ran (,)))) |
| 43 | 9, 42 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐵[,)+∞) ∈
(Clsd‘(topGen‘ran (,)))) |
| 44 | 1 | fveq2i 6909 |
. . . 4
⊢
(Clsd‘𝐾) =
(Clsd‘(topGen‘ran (,))) |
| 45 | 43, 44 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → (𝐵[,)+∞) ∈ (Clsd‘𝐾)) |
| 46 | | cnclima 23276 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐵[,)+∞) ∈ (Clsd‘𝐾)) → (◡𝐹 “ (𝐵[,)+∞)) ∈ (Clsd‘𝐽)) |
| 47 | 4, 45, 46 | syl2anc 584 |
. 2
⊢ (𝜑 → (◡𝐹 “ (𝐵[,)+∞)) ∈ (Clsd‘𝐽)) |
| 48 | 41, 47 | eqeltrrd 2842 |
1
⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) |