Metamath Proof Explorer

Theorem iooelexlt

Description: An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020)

Ref Expression
Assertion iooelexlt ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )

Proof

Step Hyp Ref Expression
1 eliooxr ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
2 1 simpld ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 ∈ ℝ* )
3 elxr ⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
4 19.3v ⊢ ( ∀ 𝑦 ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) ↔ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) )
5 ovex ⊢ ( ( 𝐴 + 𝑋 ) / 2 ) ∈ V
6 nfcv ⊢ Ⅎ 𝑦 ( ( 𝐴 + 𝑋 ) / 2 )
7 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋
8 elioore ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → 𝑋 ∈ ℝ )
9 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝐴 + 𝑋 ) ∈ ℝ )
10 9 rehalfcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ )
11 8 10 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ )
12 11 ancoms ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ )
13 12 rexrd ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ* )
14 eliooord ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑋 ∧ 𝑋 < 𝐵 ) )
15 14 simpld ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 < 𝑋 )
16 15 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝐴 < 𝑋 )
17 avglt1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝐴 < 𝑋 ↔ 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) ) )
18 8 17 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 < 𝑋 ↔ 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) ) )
19 18 ancoms ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 < 𝑋 ↔ 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) ) )
20 16 19 mpbid ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) )
21 8 rexrd ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → 𝑋 ∈ ℝ* )
22 21 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝑋 ∈ ℝ* )
23 1 simprd ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → 𝐵 ∈ ℝ* )
24 23 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℝ* )
25 avglt2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝐴 < 𝑋 ↔ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 ) )
26 8 25 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 < 𝑋 ↔ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 ) )
27 26 ancoms ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 < 𝑋 ↔ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 ) )
28 16 27 mpbid ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 )
29 14 simprd ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → 𝑋 < 𝐵 )
30 29 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝑋 < 𝐵 )
31 13 22 24 28 30 xrlttrd ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) / 2 ) < 𝐵 )
32 elioo1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ* ∧ 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) ∧ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝐵 ) ) )
33 1 32 syl ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ* ∧ 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) ∧ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝐵 ) ) )
34 33 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ℝ* ∧ 𝐴 < ( ( 𝐴 + 𝑋 ) / 2 ) ∧ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝐵 ) ) )
35 13 20 31 34 mpbir3and ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) )
36 35 28 jca ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 ) )
37 eleq1 ⊢ ( 𝑦 = ( ( 𝐴 + 𝑋 ) / 2 ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ) )
38 breq1 ⊢ ( 𝑦 = ( ( 𝐴 + 𝑋 ) / 2 ) → ( 𝑦 < 𝑋 ↔ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 ) )
39 37 38 anbi12d ⊢ ( 𝑦 = ( ( 𝐴 + 𝑋 ) / 2 ) → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 < 𝑋 ) ↔ ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( 𝐴 + 𝑋 ) / 2 ) < 𝑋 ) ) )
40 36 39 imbitrrid ⊢ ( 𝑦 = ( ( 𝐴 + 𝑋 ) / 2 ) → ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 < 𝑋 ) ) )
41 rspe ⊢ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 < 𝑋 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
42 40 41 syl6 ⊢ ( 𝑦 = ( ( 𝐴 + 𝑋 ) / 2 ) → ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
43 6 7 42 spcimgf ⊢ ( ( ( 𝐴 + 𝑋 ) / 2 ) ∈ V → ( ∀ 𝑦 ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
44 5 43 ax-mp ⊢ ( ∀ 𝑦 ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
45 4 44 sylbir ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
46 45 expcom ⊢ ( 𝐴 ∈ ℝ → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
47 simpl ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = +∞ ) → 𝑋 ∈ ( 𝐴 (,) 𝐵 ) )
48 oveq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 (,) 𝐵 ) = ( +∞ (,) 𝐵 ) )
49 48 eleq2d ⊢ ( 𝐴 = +∞ → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝑋 ∈ ( +∞ (,) 𝐵 ) ) )
50 49 adantl ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝑋 ∈ ( +∞ (,) 𝐵 ) ) )
51 pnfxr ⊢ +∞ ∈ ℝ*
52 elioo2 ⊢ ( ( +∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑋 ∈ ( +∞ (,) 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵 ) ) )
53 51 52 mpan ⊢ ( 𝐵 ∈ ℝ* → ( 𝑋 ∈ ( +∞ (,) 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵 ) ) )
54 53 biimpd ⊢ ( 𝐵 ∈ ℝ* → ( 𝑋 ∈ ( +∞ (,) 𝐵 ) → ( 𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵 ) ) )
55 elioore ⊢ ( 𝑋 ∈ ( +∞ (,) 𝐵 ) → 𝑋 ∈ ℝ )
56 rexr ⊢ ( 𝑋 ∈ ℝ → 𝑋 ∈ ℝ* )
57 pnfnlt ⊢ ( 𝑋 ∈ ℝ* → ¬ +∞ < 𝑋 )
58 56 57 syl ⊢ ( 𝑋 ∈ ℝ → ¬ +∞ < 𝑋 )
59 58 intn3an2d ⊢ ( 𝑋 ∈ ℝ → ¬ ( 𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵 ) )
60 55 59 syl ⊢ ( 𝑋 ∈ ( +∞ (,) 𝐵 ) → ¬ ( 𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵 ) )
61 60 a1i ⊢ ( 𝐵 ∈ ℝ* → ( 𝑋 ∈ ( +∞ (,) 𝐵 ) → ¬ ( 𝑋 ∈ ℝ ∧ +∞ < 𝑋 ∧ 𝑋 < 𝐵 ) ) )
62 54 61 pm2.65d ⊢ ( 𝐵 ∈ ℝ* → ¬ 𝑋 ∈ ( +∞ (,) 𝐵 ) )
63 23 62 syl ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑋 ∈ ( +∞ (,) 𝐵 ) )
64 63 pm2.21d ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑋 ∈ ( +∞ (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
65 64 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝑋 ∈ ( +∞ (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
66 50 65 sylbid ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
67 47 66 mpd ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = +∞ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
68 67 expcom ⊢ ( 𝐴 = +∞ → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
69 19.3v ⊢ ( ∀ 𝑦 ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) ↔ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) )
70 ovex ⊢ ( 𝑋 − 1 ) ∈ V
71 nfcv ⊢ Ⅎ 𝑦 ( 𝑋 − 1 )
72 peano2rem ⊢ ( 𝑋 ∈ ℝ → ( 𝑋 − 1 ) ∈ ℝ )
73 8 72 syl ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑋 − 1 ) ∈ ℝ )
74 mnflt ⊢ ( ( 𝑋 − 1 ) ∈ ℝ → -∞ < ( 𝑋 − 1 ) )
75 73 74 syl ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → -∞ < ( 𝑋 − 1 ) )
76 73 rexrd ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑋 − 1 ) ∈ ℝ* )
77 8 ltm1d ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑋 − 1 ) < 𝑋 )
78 76 21 23 77 29 xrlttrd ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑋 − 1 ) < 𝐵 )
79 mnfxr ⊢ -∞ ∈ ℝ*
80 elioo2 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( ( 𝑋 − 1 ) ∈ ℝ ∧ -∞ < ( 𝑋 − 1 ) ∧ ( 𝑋 − 1 ) < 𝐵 ) ) )
81 79 80 mpan ⊢ ( 𝐵 ∈ ℝ* → ( ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( ( 𝑋 − 1 ) ∈ ℝ ∧ -∞ < ( 𝑋 − 1 ) ∧ ( 𝑋 − 1 ) < 𝐵 ) ) )
82 23 81 syl ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) ↔ ( ( 𝑋 − 1 ) ∈ ℝ ∧ -∞ < ( 𝑋 − 1 ) ∧ ( 𝑋 − 1 ) < 𝐵 ) ) )
83 73 75 78 82 mpbir3and ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) )
84 83 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) )
85 oveq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 (,) 𝐵 ) = ( -∞ (,) 𝐵 ) )
86 85 eleq2d ⊢ ( 𝐴 = -∞ → ( ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) ) )
87 86 adantl ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ( ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑋 − 1 ) ∈ ( -∞ (,) 𝐵 ) ) )
88 84 87 mpbird ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) )
89 77 adantr ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ( 𝑋 − 1 ) < 𝑋 )
90 88 89 jca ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ( ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝑋 − 1 ) < 𝑋 ) )
91 90 adantr ⊢ ( ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) ∧ 𝑦 = ( 𝑋 − 1 ) ) → ( ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝑋 − 1 ) < 𝑋 ) )
92 eleq1 ⊢ ( 𝑦 = ( 𝑋 − 1 ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ) )
93 breq1 ⊢ ( 𝑦 = ( 𝑋 − 1 ) → ( 𝑦 < 𝑋 ↔ ( 𝑋 − 1 ) < 𝑋 ) )
94 92 93 anbi12d ⊢ ( 𝑦 = ( 𝑋 − 1 ) → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 < 𝑋 ) ↔ ( ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝑋 − 1 ) < 𝑋 ) ) )
95 94 adantl ⊢ ( ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) ∧ 𝑦 = ( 𝑋 − 1 ) ) → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 < 𝑋 ) ↔ ( ( 𝑋 − 1 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝑋 − 1 ) < 𝑋 ) ) )
96 91 95 mpbird ⊢ ( ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) ∧ 𝑦 = ( 𝑋 − 1 ) ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 < 𝑋 ) )
97 96 41 syl ⊢ ( ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) ∧ 𝑦 = ( 𝑋 − 1 ) ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
98 97 expcom ⊢ ( 𝑦 = ( 𝑋 − 1 ) → ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
99 71 7 98 spcimgf ⊢ ( ( 𝑋 − 1 ) ∈ V → ( ∀ 𝑦 ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
100 70 99 ax-mp ⊢ ( ∀ 𝑦 ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
101 69 100 sylbir ⊢ ( ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝐴 = -∞ ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )
102 101 expcom ⊢ ( 𝐴 = -∞ → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
103 46 68 102 3jaoi ⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
104 3 103 sylbi ⊢ ( 𝐴 ∈ ℝ* → ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 ) )
105 2 104 mpcom ⊢ ( 𝑋 ∈ ( 𝐴 (,) 𝐵 ) → ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑦 < 𝑋 )