elicoelioo

Description: Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017)

		Ref	Expression
	Assertion	elicoelioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (C \in [A, B) \leftrightarrow (C = A \lor C \in (A, B)))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to A \in ℝ^{*}$
2		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to B \in ℝ^{*}$
3		simprl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to C \in [A, B)$
4		elico1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in [A, B) \leftrightarrow (C \in ℝ^{*} \land A \leq C \land C < B))$
5	4	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B)) \to (C \in ℝ^{*} \land A \leq C \land C < B)$
6	5	simp1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B)) \to C \in ℝ^{*}$
7	1 2 3 6	syl21anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to C \in ℝ^{*}$
8	5	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B)) \to A \leq C$
9	1 2 3 8	syl21anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to A \leq C$
10	1 2	jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to (A \in ℝ^{} \land B \in ℝ^{})$
11		simprr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to \neg C \in (A, B)$
12	5	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in [A, B)) \to C < B$
13	10 3 12	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to C < B$
14		elioo1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A, B) \leftrightarrow (C \in ℝ^{*} \land A < C \land C < B))$
15	14	notbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg C \in (A, B) \leftrightarrow \neg (C \in ℝ^{*} \land A < C \land C < B))$
16	15	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg C \in (A, B)) \to \neg (C \in ℝ^{*} \land A < C \land C < B)$
17		3anan32	$⊢ (C \in ℝ^{} \land A < C \land C < B) \leftrightarrow ((C \in ℝ^{} \land C < B) \land A < C)$
18	17	notbii	$⊢ \neg (C \in ℝ^{} \land A < C \land C < B) \leftrightarrow \neg ((C \in ℝ^{} \land C < B) \land A < C)$
19		imnan	$⊢ ((C \in ℝ^{} \land C < B) \to \neg A < C) \leftrightarrow \neg ((C \in ℝ^{} \land C < B) \land A < C)$
20	18 19	bitr4i	$⊢ \neg (C \in ℝ^{} \land A < C \land C < B) \leftrightarrow ((C \in ℝ^{} \land C < B) \to \neg A < C)$
21	16 20	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg C \in (A, B)) \to ((C \in ℝ^{*} \land C < B) \to \neg A < C)$
22	21	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg C \in (A, B)) \land (C \in ℝ^{*} \land C < B)) \to \neg A < C$
23	10 11 7 13 22	syl22anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to \neg A < C$
24		xeqlelt	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to (A = C \leftrightarrow (A \leq C \land \neg A < C))$
25	24	biimpar	$⊢ ((A \in ℝ^{} \land C \in ℝ^{}) \land (A \leq C \land \neg A < C)) \to A = C$
26	1 7 9 23 25	syl22anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in [A, B) \land \neg C \in (A, B))) \to A = C$
27	26	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((C \in [A, B) \land \neg C \in (A, B)) \to A = C)$
28		eqcom	$⊢ A = C \leftrightarrow C = A$
29	27 28	imbitrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((C \in [A, B) \land \neg C \in (A, B)) \to C = A)$
30		pm5.6	$⊢ ((C \in [A, B) \land \neg C \in (A, B)) \to C = A) \leftrightarrow (C \in [A, B) \to (C \in (A, B) \lor C = A))$
31	29 30	sylib	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (C \in [A, B) \to (C \in (A, B) \lor C = A))$
32		orcom	$⊢ (C \in (A, B) \lor C = A) \leftrightarrow (C = A \lor C \in (A, B))$
33	31 32	imbitrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (C \in [A, B) \to (C = A \lor C \in (A, B)))$
34		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to C = A$
35		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to A \in ℝ^{*}$
36	34 35	eqeltrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to C \in ℝ^{*}$
37	35	xrleidd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to A \leq A$
38	37 34	breqtrrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to A \leq C$
39		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to A < B$
40	34 39	eqbrtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to C < B$
41		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to B \in ℝ^{*}$
42	35 41 4	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to (C \in [A, B) \leftrightarrow (C \in ℝ^{*} \land A \leq C \land C < B))$
43	36 38 40 42	mpbir3and	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C = A) \to C \in [A, B)$
44		ioossico	$⊢ (A, B) \subseteq [A, B)$
45		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C \in (A, B)) \to C \in (A, B)$
46	44 45	sselid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land C \in (A, B)) \to C \in [A, B)$
47	43 46	jaodan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C = A \lor C \in (A, B))) \to C \in [A, B)$
48	47	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((C = A \lor C \in (A, B)) \to C \in [A, B))$
49	33 48	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (C \in [A, B) \leftrightarrow (C = A \lor C \in (A, B)))$

Metamath Proof Explorer

Theorem elicoelioo

Proof