Proof of Theorem iooelexlt
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eliooxr 13446 | . . 3
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) | 
| 2 | 1 | simpld 494 | . 2
⊢ (𝑋 ∈ (𝐴(,)𝐵) → 𝐴 ∈
ℝ*) | 
| 3 |  | elxr 13159 | . . 3
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) | 
| 4 |  | 19.3v 1980 | . . . . . 6
⊢
(∀𝑦(𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) ↔ (𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ)) | 
| 5 |  | ovex 7465 | . . . . . . 7
⊢ ((𝐴 + 𝑋) / 2) ∈ V | 
| 6 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦((𝐴 + 𝑋) / 2) | 
| 7 |  | nfre1 3284 | . . . . . . . 8
⊢
Ⅎ𝑦∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋 | 
| 8 |  | elioore 13418 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (𝐴(,)𝐵) → 𝑋 ∈ ℝ) | 
| 9 |  | readdcl 11239 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 + 𝑋) ∈ ℝ) | 
| 10 | 9 | rehalfcld 12515 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((𝐴 + 𝑋) / 2) ∈ ℝ) | 
| 11 | 8, 10 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ (𝐴(,)𝐵)) → ((𝐴 + 𝑋) / 2) ∈ ℝ) | 
| 12 | 11 | ancoms 458 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝑋) / 2) ∈ ℝ) | 
| 13 | 12 | rexrd 11312 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝑋) / 2) ∈
ℝ*) | 
| 14 |  | eliooord 13447 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑋 ∧ 𝑋 < 𝐵)) | 
| 15 | 14 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑋) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → 𝐴 < 𝑋) | 
| 17 |  | avglt1 12506 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ 𝐴 < ((𝐴 + 𝑋) / 2))) | 
| 18 | 8, 17 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐴 < 𝑋 ↔ 𝐴 < ((𝐴 + 𝑋) / 2))) | 
| 19 | 18 | ancoms 458 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → (𝐴 < 𝑋 ↔ 𝐴 < ((𝐴 + 𝑋) / 2))) | 
| 20 | 16, 19 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → 𝐴 < ((𝐴 + 𝑋) / 2)) | 
| 21 | 8 | rexrd 11312 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (𝐴(,)𝐵) → 𝑋 ∈
ℝ*) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → 𝑋 ∈
ℝ*) | 
| 23 | 1 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (𝐴(,)𝐵) → 𝐵 ∈
ℝ*) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℝ*) | 
| 25 |  | avglt2 12507 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ ((𝐴 + 𝑋) / 2) < 𝑋)) | 
| 26 | 8, 25 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐴 < 𝑋 ↔ ((𝐴 + 𝑋) / 2) < 𝑋)) | 
| 27 | 26 | ancoms 458 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → (𝐴 < 𝑋 ↔ ((𝐴 + 𝑋) / 2) < 𝑋)) | 
| 28 | 16, 27 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝑋) / 2) < 𝑋) | 
| 29 | 14 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (𝐴(,)𝐵) → 𝑋 < 𝐵) | 
| 30 | 29 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → 𝑋 < 𝐵) | 
| 31 | 13, 22, 24, 28, 30 | xrlttrd 13202 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝑋) / 2) < 𝐵) | 
| 32 |  | elioo1 13428 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵) ↔ (((𝐴 + 𝑋) / 2) ∈ ℝ* ∧
𝐴 < ((𝐴 + 𝑋) / 2) ∧ ((𝐴 + 𝑋) / 2) < 𝐵))) | 
| 33 | 1, 32 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵) ↔ (((𝐴 + 𝑋) / 2) ∈ ℝ* ∧
𝐴 < ((𝐴 + 𝑋) / 2) ∧ ((𝐴 + 𝑋) / 2) < 𝐵))) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → (((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵) ↔ (((𝐴 + 𝑋) / 2) ∈ ℝ* ∧
𝐴 < ((𝐴 + 𝑋) / 2) ∧ ((𝐴 + 𝑋) / 2) < 𝐵))) | 
| 35 | 13, 20, 31, 34 | mpbir3and 1342 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵)) | 
| 36 | 35, 28 | jca 511 | . . . . . . . . . 10
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → (((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵) ∧ ((𝐴 + 𝑋) / 2) < 𝑋)) | 
| 37 |  | eleq1 2828 | . . . . . . . . . . 11
⊢ (𝑦 = ((𝐴 + 𝑋) / 2) → (𝑦 ∈ (𝐴(,)𝐵) ↔ ((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵))) | 
| 38 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑦 = ((𝐴 + 𝑋) / 2) → (𝑦 < 𝑋 ↔ ((𝐴 + 𝑋) / 2) < 𝑋)) | 
| 39 | 37, 38 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑦 = ((𝐴 + 𝑋) / 2) → ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑦 < 𝑋) ↔ (((𝐴 + 𝑋) / 2) ∈ (𝐴(,)𝐵) ∧ ((𝐴 + 𝑋) / 2) < 𝑋))) | 
| 40 | 36, 39 | imbitrrid 246 | . . . . . . . . 9
⊢ (𝑦 = ((𝐴 + 𝑋) / 2) → ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑦 < 𝑋))) | 
| 41 |  | rspe 3248 | . . . . . . . . 9
⊢ ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑦 < 𝑋) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 42 | 40, 41 | syl6 35 | . . . . . . . 8
⊢ (𝑦 = ((𝐴 + 𝑋) / 2) → ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 43 | 6, 7, 42 | spcimgf 3549 | . . . . . . 7
⊢ (((𝐴 + 𝑋) / 2) ∈ V → (∀𝑦(𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 44 | 5, 43 | ax-mp 5 | . . . . . 6
⊢
(∀𝑦(𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 45 | 4, 44 | sylbir 235 | . . . . 5
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 ∈ ℝ) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 46 | 45 | expcom 413 | . . . 4
⊢ (𝐴 ∈ ℝ → (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 47 |  | simpl 482 | . . . . . 6
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = +∞) → 𝑋 ∈ (𝐴(,)𝐵)) | 
| 48 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝐴 = +∞ → (𝐴(,)𝐵) = (+∞(,)𝐵)) | 
| 49 | 48 | eleq2d 2826 | . . . . . . . 8
⊢ (𝐴 = +∞ → (𝑋 ∈ (𝐴(,)𝐵) ↔ 𝑋 ∈ (+∞(,)𝐵))) | 
| 50 | 49 | adantl 481 | . . . . . . 7
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = +∞) → (𝑋 ∈ (𝐴(,)𝐵) ↔ 𝑋 ∈ (+∞(,)𝐵))) | 
| 51 |  | pnfxr 11316 | . . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* | 
| 52 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢
((+∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑋 ∈ (+∞(,)𝐵) ↔ (𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵))) | 
| 53 | 51, 52 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ*
→ (𝑋 ∈
(+∞(,)𝐵) ↔
(𝑋 ∈ ℝ ∧
+∞ < 𝑋 ∧ 𝑋 < 𝐵))) | 
| 54 | 53 | biimpd 229 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝑋 ∈
(+∞(,)𝐵) →
(𝑋 ∈ ℝ ∧
+∞ < 𝑋 ∧ 𝑋 < 𝐵))) | 
| 55 |  | elioore 13418 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ (+∞(,)𝐵) → 𝑋 ∈ ℝ) | 
| 56 |  | rexr 11308 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℝ → 𝑋 ∈
ℝ*) | 
| 57 |  | pnfnlt 13171 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℝ*
→ ¬ +∞ < 𝑋) | 
| 58 | 56, 57 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℝ → ¬
+∞ < 𝑋) | 
| 59 | 58 | intn3an2d 1481 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℝ → ¬
(𝑋 ∈ ℝ ∧
+∞ < 𝑋 ∧ 𝑋 < 𝐵)) | 
| 60 | 55, 59 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ (+∞(,)𝐵) → ¬ (𝑋 ∈ ℝ ∧ +∞
< 𝑋 ∧ 𝑋 < 𝐵)) | 
| 61 | 60 | a1i 11 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝑋 ∈
(+∞(,)𝐵) → ¬
(𝑋 ∈ ℝ ∧
+∞ < 𝑋 ∧ 𝑋 < 𝐵))) | 
| 62 | 54, 61 | pm2.65d 196 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ ¬ 𝑋 ∈
(+∞(,)𝐵)) | 
| 63 | 23, 62 | syl 17 | . . . . . . . . 9
⊢ (𝑋 ∈ (𝐴(,)𝐵) → ¬ 𝑋 ∈ (+∞(,)𝐵)) | 
| 64 | 63 | pm2.21d 121 | . . . . . . . 8
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝑋 ∈ (+∞(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 65 | 64 | adantr 480 | . . . . . . 7
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = +∞) → (𝑋 ∈ (+∞(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 66 | 50, 65 | sylbid 240 | . . . . . 6
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = +∞) → (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 67 | 47, 66 | mpd 15 | . . . . 5
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = +∞) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 68 | 67 | expcom 413 | . . . 4
⊢ (𝐴 = +∞ → (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 69 |  | 19.3v 1980 | . . . . . 6
⊢
(∀𝑦(𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) ↔ (𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞)) | 
| 70 |  | ovex 7465 | . . . . . . 7
⊢ (𝑋 − 1) ∈
V | 
| 71 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦(𝑋 − 1) | 
| 72 |  | peano2rem 11577 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ ℝ → (𝑋 − 1) ∈
ℝ) | 
| 73 | 8, 72 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝑋 − 1) ∈ ℝ) | 
| 74 |  | mnflt 13166 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑋 − 1) ∈ ℝ
→ -∞ < (𝑋
− 1)) | 
| 75 | 73, 74 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐴(,)𝐵) → -∞ < (𝑋 − 1)) | 
| 76 | 73 | rexrd 11312 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝑋 − 1) ∈
ℝ*) | 
| 77 | 8 | ltm1d 12201 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝑋 − 1) < 𝑋) | 
| 78 | 76, 21, 23, 77, 29 | xrlttrd 13202 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝑋 − 1) < 𝐵) | 
| 79 |  | mnfxr 11319 | . . . . . . . . . . . . . . . . . 18
⊢ -∞
∈ ℝ* | 
| 80 |  | elioo2 13429 | . . . . . . . . . . . . . . . . . 18
⊢
((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝑋 − 1) ∈
(-∞(,)𝐵) ↔
((𝑋 − 1) ∈
ℝ ∧ -∞ < (𝑋 − 1) ∧ (𝑋 − 1) < 𝐵))) | 
| 81 | 79, 80 | mpan 690 | . . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℝ*
→ ((𝑋 − 1)
∈ (-∞(,)𝐵)
↔ ((𝑋 − 1)
∈ ℝ ∧ -∞ < (𝑋 − 1) ∧ (𝑋 − 1) < 𝐵))) | 
| 82 | 23, 81 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐴(,)𝐵) → ((𝑋 − 1) ∈ (-∞(,)𝐵) ↔ ((𝑋 − 1) ∈ ℝ ∧ -∞
< (𝑋 − 1) ∧
(𝑋 − 1) < 𝐵))) | 
| 83 | 73, 75, 78, 82 | mpbir3and 1342 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (𝐴(,)𝐵) → (𝑋 − 1) ∈ (-∞(,)𝐵)) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → (𝑋 − 1) ∈ (-∞(,)𝐵)) | 
| 85 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 = -∞ → (𝐴(,)𝐵) = (-∞(,)𝐵)) | 
| 86 | 85 | eleq2d 2826 | . . . . . . . . . . . . . . 15
⊢ (𝐴 = -∞ → ((𝑋 − 1) ∈ (𝐴(,)𝐵) ↔ (𝑋 − 1) ∈ (-∞(,)𝐵))) | 
| 87 | 86 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → ((𝑋 − 1) ∈ (𝐴(,)𝐵) ↔ (𝑋 − 1) ∈ (-∞(,)𝐵))) | 
| 88 | 84, 87 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → (𝑋 − 1) ∈ (𝐴(,)𝐵)) | 
| 89 | 77 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → (𝑋 − 1) < 𝑋) | 
| 90 | 88, 89 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → ((𝑋 − 1) ∈ (𝐴(,)𝐵) ∧ (𝑋 − 1) < 𝑋)) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) ∧ 𝑦 = (𝑋 − 1)) → ((𝑋 − 1) ∈ (𝐴(,)𝐵) ∧ (𝑋 − 1) < 𝑋)) | 
| 92 |  | eleq1 2828 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝑋 − 1) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑋 − 1) ∈ (𝐴(,)𝐵))) | 
| 93 |  | breq1 5145 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝑋 − 1) → (𝑦 < 𝑋 ↔ (𝑋 − 1) < 𝑋)) | 
| 94 | 92, 93 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑋 − 1) → ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑦 < 𝑋) ↔ ((𝑋 − 1) ∈ (𝐴(,)𝐵) ∧ (𝑋 − 1) < 𝑋))) | 
| 95 | 94 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) ∧ 𝑦 = (𝑋 − 1)) → ((𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑦 < 𝑋) ↔ ((𝑋 − 1) ∈ (𝐴(,)𝐵) ∧ (𝑋 − 1) < 𝑋))) | 
| 96 | 91, 95 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) ∧ 𝑦 = (𝑋 − 1)) → (𝑦 ∈ (𝐴(,)𝐵) ∧ 𝑦 < 𝑋)) | 
| 97 | 96, 41 | syl 17 | . . . . . . . . 9
⊢ (((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) ∧ 𝑦 = (𝑋 − 1)) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 98 | 97 | expcom 413 | . . . . . . . 8
⊢ (𝑦 = (𝑋 − 1) → ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 99 | 71, 7, 98 | spcimgf 3549 | . . . . . . 7
⊢ ((𝑋 − 1) ∈ V →
(∀𝑦(𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 100 | 70, 99 | ax-mp 5 | . . . . . 6
⊢
(∀𝑦(𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 101 | 69, 100 | sylbir 235 | . . . . 5
⊢ ((𝑋 ∈ (𝐴(,)𝐵) ∧ 𝐴 = -∞) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | 
| 102 | 101 | expcom 413 | . . . 4
⊢ (𝐴 = -∞ → (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 103 | 46, 68, 102 | 3jaoi 1429 | . . 3
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 104 | 3, 103 | sylbi 217 | . 2
⊢ (𝐴 ∈ ℝ*
→ (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)) | 
| 105 | 2, 104 | mpcom 38 | 1
⊢ (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) |