Proof of Theorem icorempo
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | icorempo.1 | . 2
⊢ 𝐹 = ([,) ↾ (ℝ ×
ℝ)) | 
| 2 |  | df-ico 13393 | . . . 4
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 3 | 2 | reseq1i 5993 | . . 3
⊢ ([,)
↾ (ℝ × ℝ)) = ((𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ ×
ℝ)) | 
| 4 |  | ressxr 11305 | . . . 4
⊢ ℝ
⊆ ℝ* | 
| 5 |  | resmpo 7553 | . . . 4
⊢ ((ℝ
⊆ ℝ* ∧ ℝ ⊆ ℝ*) →
((𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ × ℝ)) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) | 
| 6 | 4, 4, 5 | mp2an 692 | . . 3
⊢ ((𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ × ℝ)) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 7 | 3, 6 | eqtri 2765 | . 2
⊢ ([,)
↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 8 |  | nfv 1914 | . . . 4
⊢
Ⅎ𝑧(𝑥 ∈ ℝ ∧ 𝑦 ∈
ℝ) | 
| 9 |  | nfrab1 3457 | . . . 4
⊢
Ⅎ𝑧{𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} | 
| 10 |  | nfrab1 3457 | . . . 4
⊢
Ⅎ𝑧{𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} | 
| 11 |  | rabid 3458 | . . . . . . . 8
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ↔ (𝑧 ∈ ℝ* ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦))) | 
| 12 |  | rexr 11307 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 13 |  | nltmnf 13171 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 <
-∞) | 
| 14 | 12, 13 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → ¬
𝑥 <
-∞) | 
| 15 |  | renemnf 11310 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → 𝑥 ≠ -∞) | 
| 16 | 15 | neneqd 2945 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → ¬
𝑥 =
-∞) | 
| 17 | 14, 16 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → (¬
𝑥 < -∞ ∧ ¬
𝑥 =
-∞)) | 
| 18 |  | pm4.56 991 | . . . . . . . . . . . . . . 15
⊢ ((¬
𝑥 < -∞ ∧ ¬
𝑥 = -∞) ↔ ¬
(𝑥 < -∞ ∨ 𝑥 = -∞)) | 
| 19 | 17, 18 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → ¬
(𝑥 < -∞ ∨ 𝑥 = -∞)) | 
| 20 |  | mnfxr 11318 | . . . . . . . . . . . . . . 15
⊢ -∞
∈ ℝ* | 
| 21 |  | xrleloe 13186 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ -∞ ∈ ℝ*) → (𝑥 ≤ -∞ ↔ (𝑥 < -∞ ∨ 𝑥 = -∞))) | 
| 22 | 12, 20, 21 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (𝑥 ≤ -∞ ↔ (𝑥 < -∞ ∨ 𝑥 = -∞))) | 
| 23 | 19, 22 | mtbird 325 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → ¬
𝑥 ≤
-∞) | 
| 24 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢ (𝑧 = -∞ → (𝑥 ≤ 𝑧 ↔ 𝑥 ≤ -∞)) | 
| 25 | 24 | notbid 318 | . . . . . . . . . . . . 13
⊢ (𝑧 = -∞ → (¬ 𝑥 ≤ 𝑧 ↔ ¬ 𝑥 ≤ -∞)) | 
| 26 | 23, 25 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑧 = -∞ → ¬ 𝑥 ≤ 𝑧)) | 
| 27 | 26 | con2d 134 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥 ≤ 𝑧 → ¬ 𝑧 = -∞)) | 
| 28 |  | rexr 11307 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) | 
| 29 |  | pnfnlt 13170 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ¬ +∞ < 𝑦) | 
| 30 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = +∞ → (𝑧 < 𝑦 ↔ +∞ < 𝑦)) | 
| 31 | 30 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑧 = +∞ → (¬ 𝑧 < 𝑦 ↔ ¬ +∞ < 𝑦)) | 
| 32 | 29, 31 | syl5ibrcom 247 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (𝑧 = +∞ →
¬ 𝑧 < 𝑦)) | 
| 33 | 32 | con2d 134 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑧 < 𝑦 → ¬ 𝑧 = +∞)) | 
| 34 | 28, 33 | syl 17 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → (𝑧 < 𝑦 → ¬ 𝑧 = +∞)) | 
| 35 | 27, 34 | im2anan9 620 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦) → (¬ 𝑧 = -∞ ∧ ¬ 𝑧 = +∞))) | 
| 36 | 35 | anim2d 612 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ*
∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)) → (𝑧 ∈ ℝ* ∧ (¬
𝑧 = -∞ ∧ ¬
𝑧 =
+∞)))) | 
| 37 |  | renepnf 11309 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ → 𝑧 ≠ +∞) | 
| 38 | 37 | neneqd 2945 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ → ¬
𝑧 =
+∞) | 
| 39 | 38 | pm4.71i 559 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ ¬
𝑧 =
+∞)) | 
| 40 |  | xrnemnf 13159 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ*
∧ 𝑧 ≠ -∞)
↔ (𝑧 ∈ ℝ
∨ 𝑧 =
+∞)) | 
| 41 | 40 | anbi1i 624 | . . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ*
∧ 𝑧 ≠ -∞)
∧ ¬ 𝑧 = +∞)
↔ ((𝑧 ∈ ℝ
∨ 𝑧 = +∞) ∧
¬ 𝑧 =
+∞)) | 
| 42 |  | df-ne 2941 | . . . . . . . . . . . . 13
⊢ (𝑧 ≠ -∞ ↔ ¬
𝑧 =
-∞) | 
| 43 | 42 | anbi2i 623 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ*
∧ 𝑧 ≠ -∞)
↔ (𝑧 ∈
ℝ* ∧ ¬ 𝑧 = -∞)) | 
| 44 | 43 | anbi1i 624 | . . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ*
∧ 𝑧 ≠ -∞)
∧ ¬ 𝑧 = +∞)
↔ ((𝑧 ∈
ℝ* ∧ ¬ 𝑧 = -∞) ∧ ¬ 𝑧 = +∞)) | 
| 45 |  | pm5.61 1003 | . . . . . . . . . . 11
⊢ (((𝑧 ∈ ℝ ∨ 𝑧 = +∞) ∧ ¬ 𝑧 = +∞) ↔ (𝑧 ∈ ℝ ∧ ¬
𝑧 =
+∞)) | 
| 46 | 41, 44, 45 | 3bitr3i 301 | . . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ*
∧ ¬ 𝑧 = -∞)
∧ ¬ 𝑧 = +∞)
↔ (𝑧 ∈ ℝ
∧ ¬ 𝑧 =
+∞)) | 
| 47 |  | anass 468 | . . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ*
∧ ¬ 𝑧 = -∞)
∧ ¬ 𝑧 = +∞)
↔ (𝑧 ∈
ℝ* ∧ (¬ 𝑧 = -∞ ∧ ¬ 𝑧 = +∞))) | 
| 48 | 39, 46, 47 | 3bitr2ri 300 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℝ*
∧ (¬ 𝑧 = -∞
∧ ¬ 𝑧 = +∞))
↔ 𝑧 ∈
ℝ) | 
| 49 | 36, 48 | imbitrdi 251 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ*
∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)) → 𝑧 ∈ ℝ)) | 
| 50 | 11, 49 | biimtrid 242 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → 𝑧 ∈ ℝ)) | 
| 51 | 11 | simprbi 496 | . . . . . . . 8
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)) | 
| 52 | 51 | a1i 11 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦))) | 
| 53 | 50, 52 | jcad 512 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)))) | 
| 54 |  | rabid 3458 | . . . . . 6
⊢ (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ↔ (𝑧 ∈ ℝ ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦))) | 
| 55 | 53, 54 | imbitrrdi 252 | . . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) | 
| 56 |  | rabss2 4078 | . . . . . . 7
⊢ (ℝ
⊆ ℝ* → {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ⊆ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 57 | 4, 56 | ax-mp 5 | . . . . . 6
⊢ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ⊆ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} | 
| 58 | 57 | sseli 3979 | . . . . 5
⊢ (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 59 | 55, 58 | impbid1 225 | . . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ↔ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) | 
| 60 | 8, 9, 10, 59 | eqrd 4003 | . . 3
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} = {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 61 | 60 | mpoeq3ia 7511 | . 2
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 62 | 1, 7, 61 | 3eqtri 2769 | 1
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |