Step |
Hyp |
Ref |
Expression |
1 |
|
iocopn.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
2 |
|
iocopn.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ* ) |
3 |
|
iocopn.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
4 |
|
iocopn.k |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
5 |
|
iocopn.j |
⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 (,] 𝐵 ) ) |
6 |
|
iocopn.alec |
⊢ ( 𝜑 → 𝐴 ≤ 𝐶 ) |
7 |
|
iocopn.6 |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
8 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
9 |
4 8
|
eqeltri |
⊢ 𝐾 ∈ Top |
10 |
9
|
a1i |
⊢ ( 𝜑 → 𝐾 ∈ Top ) |
11 |
|
ovexd |
⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ∈ V ) |
12 |
|
iooretop |
⊢ ( 𝐶 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) |
13 |
12 4
|
eleqtrri |
⊢ ( 𝐶 (,) +∞ ) ∈ 𝐾 |
14 |
13
|
a1i |
⊢ ( 𝜑 → ( 𝐶 (,) +∞ ) ∈ 𝐾 ) |
15 |
|
elrestr |
⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐴 (,] 𝐵 ) ∈ V ∧ ( 𝐶 (,) +∞ ) ∈ 𝐾 ) → ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ∈ ( 𝐾 ↾t ( 𝐴 (,] 𝐵 ) ) ) |
16 |
10 11 14 15
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ∈ ( 𝐾 ↾t ( 𝐴 (,] 𝐵 ) ) ) |
17 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐶 ∈ ℝ* ) |
18 |
3
|
rexrd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ* ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐵 ∈ ℝ* ) |
20 |
|
elinel1 |
⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐶 (,) +∞ ) ) |
21 |
|
elioore |
⊢ ( 𝑥 ∈ ( 𝐶 (,) +∞ ) → 𝑥 ∈ ℝ ) |
22 |
20 21
|
syl |
⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ℝ ) |
23 |
22
|
rexrd |
⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ℝ* ) |
24 |
23
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ℝ* ) |
25 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
26 |
25
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → +∞ ∈ ℝ* ) |
27 |
20
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐶 (,) +∞ ) ) |
28 |
|
ioogtlb |
⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ ( 𝐶 (,) +∞ ) ) → 𝐶 < 𝑥 ) |
29 |
17 26 27 28
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐶 < 𝑥 ) |
30 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝐴 ∈ ℝ* ) |
31 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ) |
33 |
|
iocleub |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ≤ 𝐵 ) |
34 |
30 19 32 33
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ≤ 𝐵 ) |
35 |
17 19 24 29 34
|
eliocd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) |
36 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐶 ∈ ℝ* ) |
37 |
25
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → +∞ ∈ ℝ* ) |
38 |
|
iocssre |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐶 (,] 𝐵 ) ⊆ ℝ ) |
39 |
2 7 38
|
syl2anc |
⊢ ( 𝜑 → ( 𝐶 (,] 𝐵 ) ⊆ ℝ ) |
40 |
39
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ℝ ) |
41 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐵 ∈ ℝ* ) |
42 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) |
43 |
|
iocgtlb |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐶 < 𝑥 ) |
44 |
36 41 42 43
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐶 < 𝑥 ) |
45 |
40
|
ltpnfd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 < +∞ ) |
46 |
36 37 40 44 45
|
eliood |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐶 (,) +∞ ) ) |
47 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 ∈ ℝ* ) |
48 |
40
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ℝ* ) |
49 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 ≤ 𝐶 ) |
50 |
47 36 48 49 44
|
xrlelttrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝐴 < 𝑥 ) |
51 |
|
iocleub |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ≤ 𝐵 ) |
52 |
36 41 42 51
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ≤ 𝐵 ) |
53 |
47 41 48 50 52
|
eliocd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ) |
54 |
46 53
|
elind |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) → 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ) |
55 |
35 54
|
impbida |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) ↔ 𝑥 ∈ ( 𝐶 (,] 𝐵 ) ) ) |
56 |
55
|
eqrdv |
⊢ ( 𝜑 → ( ( 𝐶 (,) +∞ ) ∩ ( 𝐴 (,] 𝐵 ) ) = ( 𝐶 (,] 𝐵 ) ) |
57 |
5
|
eqcomi |
⊢ ( 𝐾 ↾t ( 𝐴 (,] 𝐵 ) ) = 𝐽 |
58 |
57
|
a1i |
⊢ ( 𝜑 → ( 𝐾 ↾t ( 𝐴 (,] 𝐵 ) ) = 𝐽 ) |
59 |
16 56 58
|
3eltr3d |
⊢ ( 𝜑 → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 ) |