icoopnst

Description: A half-open interval starting at A is open in the closed interval from A to B . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Hypothesis	icoopnst.1	$⊢ J = MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])})$
	Assertion	icoopnst	$⊢ (A \in ℝ \land B \in ℝ) \to (C \in (A, B] \to [A, C) \in J)$

Proof

Step	Hyp	Ref	Expression
1		icoopnst.1	$⊢ J = MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])})$
2		iooretop	$⊢ (A - 1, C) \in topGen (ran (.))$
3		simp1	$⊢ (v \in ℝ \land A \leq v \land v < C) \to v \in ℝ$
4	3	a1i	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to v \in ℝ)$
5		ltm1	$⊢ A \in ℝ \to A - 1 < A$
6	5	adantr	$⊢ (A \in ℝ \land v \in ℝ) \to A - 1 < A$
7		peano2rem	$⊢ A \in ℝ \to A - 1 \in ℝ$
8	7	adantr	$⊢ (A \in ℝ \land v \in ℝ) \to A - 1 \in ℝ$
9		ltletr	$⊢ (A - 1 \in ℝ \land A \in ℝ \land v \in ℝ) \to ((A - 1 < A \land A \leq v) \to A - 1 < v)$
10	9	3expb	$⊢ (A - 1 \in ℝ \land (A \in ℝ \land v \in ℝ)) \to ((A - 1 < A \land A \leq v) \to A - 1 < v)$
11	8 10	mpancom	$⊢ (A \in ℝ \land v \in ℝ) \to ((A - 1 < A \land A \leq v) \to A - 1 < v)$
12	6 11	mpand	$⊢ (A \in ℝ \land v \in ℝ) \to (A \leq v \to A - 1 < v)$
13	12	impr	$⊢ (A \in ℝ \land (v \in ℝ \land A \leq v)) \to A - 1 < v$
14	13	3adantr3	$⊢ (A \in ℝ \land (v \in ℝ \land A \leq v \land v < C)) \to A - 1 < v$
15	14	ex	$⊢ A \in ℝ \to ((v \in ℝ \land A \leq v \land v < C) \to A - 1 < v)$
16	15	ad2antrr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to A - 1 < v)$
17		simp3	$⊢ (v \in ℝ \land A \leq v \land v < C) \to v < C$
18	17	a1i	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to v < C)$
19	4 16 18	3jcad	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to (v \in ℝ \land A - 1 < v \land v < C))$
20		simp2	$⊢ (v \in ℝ \land A \leq v \land v < C) \to A \leq v$
21	20	a1i	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to A \leq v)$
22		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
23		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (C \in (A, B] \leftrightarrow (C \in ℝ \land A < C \land C \leq B))$
24	22 23	sylan	$⊢ (A \in ℝ \land B \in ℝ) \to (C \in (A, B] \leftrightarrow (C \in ℝ \land A < C \land C \leq B))$
25	24	biimpa	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to (C \in ℝ \land A < C \land C \leq B)$
26		ltleletr	$⊢ (v \in ℝ \land C \in ℝ \land B \in ℝ) \to ((v < C \land C \leq B) \to v \leq B)$
27	26	3expa	$⊢ ((v \in ℝ \land C \in ℝ) \land B \in ℝ) \to ((v < C \land C \leq B) \to v \leq B)$
28	27	an31s	$⊢ ((B \in ℝ \land C \in ℝ) \land v \in ℝ) \to ((v < C \land C \leq B) \to v \leq B)$
29	28	imp	$⊢ (((B \in ℝ \land C \in ℝ) \land v \in ℝ) \land (v < C \land C \leq B)) \to v \leq B$
30	29	ancom2s	$⊢ (((B \in ℝ \land C \in ℝ) \land v \in ℝ) \land (C \leq B \land v < C)) \to v \leq B$
31	30	an4s	$⊢ (((B \in ℝ \land C \in ℝ) \land C \leq B) \land (v \in ℝ \land v < C)) \to v \leq B$
32	31	3adantr2	$⊢ (((B \in ℝ \land C \in ℝ) \land C \leq B) \land (v \in ℝ \land A \leq v \land v < C)) \to v \leq B$
33	32	ex	$⊢ ((B \in ℝ \land C \in ℝ) \land C \leq B) \to ((v \in ℝ \land A \leq v \land v < C) \to v \leq B)$
34	33	anasss	$⊢ (B \in ℝ \land (C \in ℝ \land C \leq B)) \to ((v \in ℝ \land A \leq v \land v < C) \to v \leq B)$
35	34	3adantr2	$⊢ (B \in ℝ \land (C \in ℝ \land A < C \land C \leq B)) \to ((v \in ℝ \land A \leq v \land v < C) \to v \leq B)$
36	35	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land A < C \land C \leq B)) \to ((v \in ℝ \land A \leq v \land v < C) \to v \leq B)$
37	25 36	syldan	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to v \leq B)$
38	4 21 37	3jcad	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to (v \in ℝ \land A \leq v \land v \leq B))$
39	19 38	jcad	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \to ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)))$
40		simpl1	$⊢ ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)) \to v \in ℝ$
41		simpr2	$⊢ ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)) \to A \leq v$
42		simpl3	$⊢ ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)) \to v < C$
43	40 41 42	3jca	$⊢ ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)) \to (v \in ℝ \land A \leq v \land v < C)$
44	39 43	impbid1	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in ℝ \land A \leq v \land v < C) \leftrightarrow ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)))$
45		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to A \in ℝ$
46	25	simp1d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to C \in ℝ$
47	46	rexrd	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to C \in ℝ^{*}$
48		elico2	$⊢ (A \in ℝ \land C \in ℝ^{*}) \to (v \in [A, C) \leftrightarrow (v \in ℝ \land A \leq v \land v < C))$
49	45 47 48	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to (v \in [A, C) \leftrightarrow (v \in ℝ \land A \leq v \land v < C))$
50		elin	$⊢ v \in ((A - 1, C) \cap [A, B]) \leftrightarrow (v \in (A - 1, C) \land v \in [A, B])$
51	7	rexrd	$⊢ A \in ℝ \to A - 1 \in ℝ^{*}$
52	51	ad2antrr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to A - 1 \in ℝ^{*}$
53		elioo2	$⊢ (A - 1 \in ℝ^{} \land C \in ℝ^{}) \to (v \in (A - 1, C) \leftrightarrow (v \in ℝ \land A - 1 < v \land v < C))$
54	52 47 53	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to (v \in (A - 1, C) \leftrightarrow (v \in ℝ \land A - 1 < v \land v < C))$
55		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (v \in [A, B] \leftrightarrow (v \in ℝ \land A \leq v \land v \leq B))$
56	55	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to (v \in [A, B] \leftrightarrow (v \in ℝ \land A \leq v \land v \leq B))$
57	54 56	anbi12d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to ((v \in (A - 1, C) \land v \in [A, B]) \leftrightarrow ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)))$
58	50 57	bitrid	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to (v \in ((A - 1, C) \cap [A, B]) \leftrightarrow ((v \in ℝ \land A - 1 < v \land v < C) \land (v \in ℝ \land A \leq v \land v \leq B)))$
59	44 49 58	3bitr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to (v \in [A, C) \leftrightarrow v \in ((A - 1, C) \cap [A, B]))$
60	59	eqrdv	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to [A, C) = (A - 1, C) \cap [A, B]$
61		ineq1	$⊢ v = (A - 1, C) \to v \cap [A, B] = (A - 1, C) \cap [A, B]$
62	61	rspceeqv	$⊢ ((A - 1, C) \in topGen (ran (.)) \land [A, C) = (A - 1, C) \cap [A, B]) \to \exists v \in topGen (ran (.)) [A, C) = v \cap [A, B]$
63	2 60 62	sylancr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to \exists v \in topGen (ran (.)) [A, C) = v \cap [A, B]$
64		retop	$⊢ topGen (ran (.)) \in Top$
65		ovex	$⊢ [A, B] \in V$
66		elrest	$⊢ (topGen (ran (.)) \in Top \land [A, B] \in V) \to ([A, C) \in (topGen (ran (.)) ↾_{𝑡} [A, B]) \leftrightarrow \exists v \in topGen (ran (.)) [A, C) = v \cap [A, B])$
67	64 65 66	mp2an	$⊢ [A, C) \in (topGen (ran (.)) ↾_{𝑡} [A, B]) \leftrightarrow \exists v \in topGen (ran (.)) [A, C) = v \cap [A, B]$
68	63 67	sylibr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to [A, C) \in (topGen (ran (.)) ↾_{𝑡} [A, B])$
69		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
70	69	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to [A, B] \subseteq ℝ$
71		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
72	71 1	resubmet	$⊢ [A, B] \subseteq ℝ \to J = topGen (ran (.)) ↾_{𝑡} [A, B]$
73	70 72	syl	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to J = topGen (ran (.)) ↾_{𝑡} [A, B]$
74	68 73	eleqtrrd	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in (A, B]) \to [A, C) \in J$
75	74	ex	$⊢ (A \in ℝ \land B \in ℝ) \to (C \in (A, B] \to [A, C) \in J)$

Metamath Proof Explorer

Theorem icoopnst

Proof