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

Proof

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

Metamath Proof Explorer

Theorem lptioo1

Proof