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 ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )