This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lptioo1

Description: The lower bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses lptioo1.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
lptioo1.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
lptioo1.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
lptioo1.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion lptioo1 ( 𝜑 → 𝐴 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lptioo1.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 lptioo1.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 lptioo1.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
4 lptioo1.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 difssd ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ⊆ ( 𝐴 (,) 𝐵 ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
7 lbioo ⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 )
8 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ) )
9 8 biimpcd ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑥 = 𝐴 → 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ) )
10 7 9 mtoi ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 = 𝐴 )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 𝐴 )
12 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
13 11 12 sylnibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 ∈ { 𝐴 } )
14 6 13 eldifd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) )
15 5 14 eqelssd ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) = ( 𝐴 (,) 𝐵 ) )
16 15 ineq2d ⊢ ( 𝜑 → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ) = ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ) = ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) )
18 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑎 ∈ ℝ* )
19 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑏 ∈ ℝ* )
20 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
21 20 3 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
23 iooin ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
24 18 19 22 23 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
25 elioo3g ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ↔ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝑎 < 𝐴 ∧ 𝐴 < 𝑏 ) ) )
26 25 biimpi ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝑎 < 𝐴 ∧ 𝐴 < 𝑏 ) ) )
27 26 simpld ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) )
28 27 simp1d ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → 𝑎 ∈ ℝ* )
29 27 simp3d ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → 𝐴 ∈ ℝ* )
30 26 simprd ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑎 < 𝐴 ∧ 𝐴 < 𝑏 ) )
31 30 simpld ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → 𝑎 < 𝐴 )
32 28 29 31 xrltled ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → 𝑎 ≤ 𝐴 )
33 32 iftrued ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝐴 )
34 33 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝐴 )
35 30 simprd ⊢ ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → 𝐴 < 𝑏 )
36 35 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑏 ≤ 𝐵 ) → 𝐴 < 𝑏 )
37 iftrue ⊢ ( 𝑏 ≤ 𝐵 → if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) = 𝑏 )
38 37 eqcomd ⊢ ( 𝑏 ≤ 𝐵 → 𝑏 = if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
39 38 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑏 ≤ 𝐵 ) → 𝑏 = if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
40 36 39 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑏 ≤ 𝐵 ) → 𝐴 < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
41 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑏 ≤ 𝐵 ) → 𝐴 < 𝐵 )
42 iffalse ⊢ ( ¬ 𝑏 ≤ 𝐵 → if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) = 𝐵 )
43 42 eqcomd ⊢ ( ¬ 𝑏 ≤ 𝐵 → 𝐵 = if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
44 43 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑏 ≤ 𝐵 ) → 𝐵 = if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
45 41 44 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑏 ≤ 𝐵 ) → 𝐴 < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
46 40 45 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝐴 < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
47 34 46 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
48 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑎 ≤ 𝐴 ) → 𝐴 ∈ ℝ* )
49 18 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑎 ≤ 𝐴 ) → 𝑎 ∈ ℝ* )
50 48 49 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) ∈ ℝ* )
51 19 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑏 ≤ 𝐵 ) → 𝑏 ∈ ℝ* )
52 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑏 ≤ 𝐵 ) → 𝐵 ∈ ℝ* )
53 51 52 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ∈ ℝ* )
54 ioon0 ⊢ ( ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) ∈ ℝ* ∧ if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ∈ ℝ* ) → ( ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) ≠ ∅ ↔ if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
55 50 53 54 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) ≠ ∅ ↔ if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
56 47 55 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) ≠ ∅ )
57 24 56 eqnetrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ )
58 17 57 eqnetrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐴 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ) ≠ ∅ )
59 58 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ) ≠ ∅ ) )
60 59 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ) ≠ ∅ ) )
61 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
62 61 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
63 1 62 2 islptre ⊢ ( 𝜑 → ( 𝐴 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) ↔ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐴 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐴 } ) ) ≠ ∅ ) ) )
64 60 63 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )