Theorem lptioo2

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

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

Proof

Step	Hyp	Ref	Expression
1		lptioo2.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		lptioo2.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
3		lptioo2.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		lptioo2.4	⊢ ( 𝜑 → 𝐴 < 𝐵 )
5		difssd	⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐵 } ) ⊆ ( 𝐴 (,) 𝐵 ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
7		ubioo	⊢ ¬ 𝐵 ∈ ( 𝐴 (,) 𝐵 )
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	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝐴 ∈ ℝ* )
21		elioo3g	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ↔ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝑎 < 𝐵 ∧ 𝐵 < 𝑏 ) ) )
22	21	biimpi	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝑎 < 𝐵 ∧ 𝐵 < 𝑏 ) ) )
23	22	simpld	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
24	23	simp3d	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → 𝐵 ∈ ℝ* )
25	24	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝐵 ∈ ℝ* )
26		iooin	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
27	18 19 20 25 26	syl22anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
28		iftrue	⊢ ( 𝑎 ≤ 𝐴 → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝐴 )
29	28	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑎 ≤ 𝐴 ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝐴 )
30	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑎 ≤ 𝐴 ) → 𝐴 < 𝐵 )
31	29 30	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ 𝑎 ≤ 𝐴 ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < 𝐵 )
32		iffalse	⊢ ( ¬ 𝑎 ≤ 𝐴 → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝑎 )
33	32	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑎 ≤ 𝐴 ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝑎 )
34	22	simprd	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑎 < 𝐵 ∧ 𝐵 < 𝑏 ) )
35	34	simpld	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → 𝑎 < 𝐵 )
36	35	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑎 ≤ 𝐴 ) → 𝑎 < 𝐵 )
37	33 36	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑎 ≤ 𝐴 ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < 𝐵 )
38	31 37	pm2.61dan	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < 𝐵 )
39	34	simprd	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → 𝐵 < 𝑏 )
40	23	simp2d	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → 𝑏 ∈ ℝ* )
41		xrltnle	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝐵 < 𝑏 ↔ ¬ 𝑏 ≤ 𝐵 ) )
42	24 40 41	syl2anc	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝐵 < 𝑏 ↔ ¬ 𝑏 ≤ 𝐵 ) )
43	39 42	mpbid	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ¬ 𝑏 ≤ 𝐵 )
44		iffalse	⊢ ( ¬ 𝑏 ≤ 𝐵 → if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) = 𝐵 )
45	43 44	syl	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) = 𝐵 )
46	45	eqcomd	⊢ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → 𝐵 = if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
47	46	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝐵 = if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
48	38 47	breqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) )
49	20 18	ifcld	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) ∈ ℝ* )
50	47 25	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ∈ ℝ* )
51		ioon0	⊢ ( ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) ∈ ℝ* ∧ if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ∈ ℝ* ) → ( ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) ≠ ∅ ↔ if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
52	49 50 51	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) ≠ ∅ ↔ if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) < if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) )
53	48 52	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( 𝑏 ≤ 𝐵 , 𝑏 , 𝐵 ) ) ≠ ∅ )
54	27 53	eqnetrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ )
55	17 54	eqnetrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) ∧ 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐵 } ) ) ≠ ∅ )
56	55	ex	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐵 } ) ) ≠ ∅ ) )
57	56	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐵 } ) ) ≠ ∅ ) )
58		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
59	58	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
60	1 59 3	islptre	⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) ↔ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝐵 } ) ) ≠ ∅ ) ) )
61	57 60	mpbird	⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )