iocinioc2

Description: Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017)

		Ref	Expression
	Assertion	iocinioc2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (A, C] \cap (B, C] = (B, C]$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in ((A, C] \cap (B, C]) \leftrightarrow (x \in (A, C] \land x \in (B, C])$
2		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to A \in ℝ^{}$
3		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to C \in ℝ^{}$
4		elioc1	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to (x \in (A, C] \leftrightarrow (x \in ℝ^{*} \land A < x \land x \leq C))$
5	2 3 4	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to (x \in (A, C] \leftrightarrow (x \in ℝ^{} \land A < x \land x \leq C))$
6		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to B \in ℝ^{}$
7		elioc1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (x \in (B, C] \leftrightarrow (x \in ℝ^{*} \land B < x \land x \leq C))$
8	6 3 7	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to (x \in (B, C] \leftrightarrow (x \in ℝ^{} \land B < x \land x \leq C))$
9	5 8	anbi12d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to ((x \in (A, C] \land x \in (B, C]) \leftrightarrow ((x \in ℝ^{} \land A < x \land x \leq C) \land (x \in ℝ^{*} \land B < x \land x \leq C)))$
10		simp31	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to x \in ℝ^{*}$
11	2	3adant3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to A \in ℝ^{*}$
12	6	3adant3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to B \in ℝ^{*}$
13		simp2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to A \leq B$
14		simp32	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to B < x$
15	11 12 10 13 14	xrlelttrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to A < x$
16		simp33	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to x \leq C$
17	10 15 16	3jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B \land (x \in ℝ^{} \land B < x \land x \leq C)) \to (x \in ℝ^{*} \land A < x \land x \leq C)$
18	17	3expia	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to ((x \in ℝ^{} \land B < x \land x \leq C) \to (x \in ℝ^{*} \land A < x \land x \leq C))$
19	18	pm4.71rd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to ((x \in ℝ^{} \land B < x \land x \leq C) \leftrightarrow ((x \in ℝ^{} \land A < x \land x \leq C) \land (x \in ℝ^{} \land B < x \land x \leq C)))$
20	9 19	bitr4d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to ((x \in (A, C] \land x \in (B, C]) \leftrightarrow (x \in ℝ^{} \land B < x \land x \leq C))$
21	1 20	syl5bb	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to (x \in ((A, C] \cap (B, C]) \leftrightarrow (x \in ℝ^{} \land B < x \land x \leq C))$
22	21 8	bitr4d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (x \in ((A, C] \cap (B, C]) \leftrightarrow x \in (B, C])$
23	22	eqrdv	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (A, C] \cap (B, C] = (B, C]$

Metamath Proof Explorer

Theorem iocinioc2

Proof