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