iocopnst

Description: A half-open interval ending at B 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	iocopnst.1	$⊢ J = MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])})$
	Assertion	iocopnst	$⊢ (A \in ℝ \land B \in ℝ) \to (C \in [A, B) \to (C, B] \in J)$

Proof

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

Metamath Proof Explorer

Theorem iocopnst

Proof