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	$⊢ J = topGen (ran (.))$
	lptioo2.2	$⊢ φ \to A \in ℝ^{*}$
	lptioo2.3	$⊢ φ \to B \in ℝ$
	lptioo2.4	$⊢ φ \to A < B$
Assertion	lptioo2	$⊢ φ \to B \in limPt (J) ((A, B))$

Proof

Step	Hyp	Ref	Expression
1		lptioo2.1	$⊢ J = topGen (ran (.))$
2		lptioo2.2	$⊢ φ \to A \in ℝ^{*}$
3		lptioo2.3	$⊢ φ \to B \in ℝ$
4		lptioo2.4	$⊢ φ \to A < B$
5		difssd	$⊢ φ \to (A, B) ∖ \{B\} \subseteq (A, B)$
6		simpr	$⊢ (φ \land x \in (A, B)) \to x \in (A, B)$
7		ubioo	$⊢ \neg B \in (A, B)$
8		eleq1	$⊢ x = B \to (x \in (A, B) \leftrightarrow B \in (A, B))$
9	8	biimpcd	$⊢ x \in (A, B) \to (x = B \to B \in (A, B))$
10	7 9	mtoi	$⊢ x \in (A, B) \to \neg x = B$
11	10	adantl	$⊢ (φ \land x \in (A, B)) \to \neg x = B$
12		velsn	$⊢ x \in \{B\} \leftrightarrow x = B$
13	11 12	sylnibr	$⊢ (φ \land x \in (A, B)) \to \neg x \in \{B\}$
14	6 13	eldifd	$⊢ (φ \land x \in (A, B)) \to x \in ((A, B) ∖ \{B\})$
15	5 14	eqelssd	$⊢ φ \to (A, B) ∖ \{B\} = (A, B)$
16	15	ineq2d	$⊢ φ \to (a, b) \cap ((A, B) ∖ \{B\}) = (a, b) \cap (A, B)$
17	16	ad2antrr	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to (a, b) \cap ((A, B) ∖ \{B\}) = (a, b) \cap (A, B)$
18		simplrl	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to a \in ℝ^{*}$
19		simplrr	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to b \in ℝ^{*}$
20	2	ad2antrr	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to A \in ℝ^{*}$
21		elioo3g	$⊢ B \in (a, b) \leftrightarrow ((a \in ℝ^{} \land b \in ℝ^{} \land B \in ℝ^{*}) \land (a < B \land B < b))$
22	21	biimpi	$⊢ B \in (a, b) \to ((a \in ℝ^{} \land b \in ℝ^{} \land B \in ℝ^{*}) \land (a < B \land B < b))$
23	22	simpld	$⊢ B \in (a, b) \to (a \in ℝ^{} \land b \in ℝ^{} \land B \in ℝ^{*})$
24	23	simp3d	$⊢ B \in (a, b) \to B \in ℝ^{*}$
25	24	adantl	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to B \in ℝ^{*}$
26		iooin	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land (A \in ℝ^{} \land B \in ℝ^{})) \to (a, b) \cap (A, B) = (if (a \leq A, A, a), if (b \leq B, b, B))$
27	18 19 20 25 26	syl22anc	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to (a, b) \cap (A, B) = (if (a \leq A, A, a), if (b \leq B, b, B))$
28		iftrue	$⊢ a \leq A \to if (a \leq A, A, a) = A$
29	28	adantl	$⊢ (((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \land a \leq A) \to if (a \leq A, A, a) = A$
30	4	ad3antrrr	$⊢ (((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \land a \leq A) \to A < B$
31	29 30	eqbrtrd	$⊢ (((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \land a \leq A) \to if (a \leq A, A, a) < B$
32		iffalse	$⊢ \neg a \leq A \to if (a \leq A, A, a) = a$
33	32	adantl	$⊢ (((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \land \neg a \leq A) \to if (a \leq A, A, a) = a$
34	22	simprd	$⊢ B \in (a, b) \to (a < B \land B < b)$
35	34	simpld	$⊢ B \in (a, b) \to a < B$
36	35	ad2antlr	$⊢ (((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \land \neg a \leq A) \to a < B$
37	33 36	eqbrtrd	$⊢ (((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \land \neg a \leq A) \to if (a \leq A, A, a) < B$
38	31 37	pm2.61dan	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to if (a \leq A, A, a) < B$
39	34	simprd	$⊢ B \in (a, b) \to B < b$
40	23	simp2d	$⊢ B \in (a, b) \to b \in ℝ^{*}$
41		xrltnle	$⊢ (B \in ℝ^{} \land b \in ℝ^{}) \to (B < b \leftrightarrow \neg b \leq B)$
42	24 40 41	syl2anc	$⊢ B \in (a, b) \to (B < b \leftrightarrow \neg b \leq B)$
43	39 42	mpbid	$⊢ B \in (a, b) \to \neg b \leq B$
44		iffalse	$⊢ \neg b \leq B \to if (b \leq B, b, B) = B$
45	43 44	syl	$⊢ B \in (a, b) \to if (b \leq B, b, B) = B$
46	45	eqcomd	$⊢ B \in (a, b) \to B = if (b \leq B, b, B)$
47	46	adantl	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to B = if (b \leq B, b, B)$
48	38 47	breqtrd	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to if (a \leq A, A, a) < if (b \leq B, b, B)$
49	20 18	ifcld	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to if (a \leq A, A, a) \in ℝ^{*}$
50	47 25	eqeltrrd	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to if (b \leq B, b, B) \in ℝ^{*}$
51		ioon0	$⊢ (if (a \leq A, A, a) \in ℝ^{} \land if (b \leq B, b, B) \in ℝ^{}) \to ((if (a \leq A, A, a), if (b \leq B, b, B)) \neq \emptyset \leftrightarrow if (a \leq A, A, a) < if (b \leq B, b, B))$
52	49 50 51	syl2anc	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to ((if (a \leq A, A, a), if (b \leq B, b, B)) \neq \emptyset \leftrightarrow if (a \leq A, A, a) < if (b \leq B, b, B))$
53	48 52	mpbird	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to (if (a \leq A, A, a), if (b \leq B, b, B)) \neq \emptyset$
54	27 53	eqnetrd	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to (a, b) \cap (A, B) \neq \emptyset$
55	17 54	eqnetrd	$⊢ ((φ \land (a \in ℝ^{} \land b \in ℝ^{})) \land B \in (a, b)) \to (a, b) \cap ((A, B) ∖ \{B\}) \neq \emptyset$
56	55	ex	$⊢ (φ \land (a \in ℝ^{} \land b \in ℝ^{})) \to (B \in (a, b) \to (a, b) \cap ((A, B) ∖ \{B\}) \neq \emptyset)$
57	56	ralrimivva	$⊢ φ \to \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap ((A, B) ∖ \{B\}) \neq \emptyset)$
58		ioossre	$⊢ (A, B) \subseteq ℝ$
59	58	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
60	1 59 3	islptre	$⊢ φ \to (B \in limPt (J) ((A, B)) \leftrightarrow \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap ((A, B) ∖ \{B\}) \neq \emptyset))$
61	57 60	mpbird	$⊢ φ \to B \in limPt (J) ((A, B))$

Metamath Proof Explorer

Theorem lptioo2

Proof