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 ⊢X∈AB→∃y∈ABy<X

Proof

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