iocinico

Description: The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		df-in	$⊢ (A, B] \cap [B, C) = \{x \| (x \in (A, B] \land x \in [B, C))\}$
2		elioc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (x \in (A, B] \leftrightarrow (x \in ℝ^{*} \land A < x \land x \leq B))$
3	2	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in (A, B] \leftrightarrow (x \in ℝ^{} \land A < x \land x \leq B))$
4		3simpb	$⊢ (x \in ℝ^{} \land A < x \land x \leq B) \to (x \in ℝ^{} \land x \leq B)$
5	3 4	syl6bi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in (A, B] \to (x \in ℝ^{} \land x \leq B))$
6		elico1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [B, C) \leftrightarrow (x \in ℝ^{*} \land B \leq x \land x < C))$
7	6	3adant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [B, C) \leftrightarrow (x \in ℝ^{} \land B \leq x \land x < C))$
8		3simpa	$⊢ (x \in ℝ^{} \land B \leq x \land x < C) \to (x \in ℝ^{} \land B \leq x)$
9	7 8	syl6bi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [B, C) \to (x \in ℝ^{} \land B \leq x))$
10	5 9	anim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to ((x \in (A, B] \land x \in [B, C)) \to ((x \in ℝ^{} \land x \leq B) \land (x \in ℝ^{*} \land B \leq x)))$
11		simpll	$⊢ ((x \in ℝ^{} \land x \leq B) \land (x \in ℝ^{} \land B \leq x)) \to x \in ℝ^{*}$
12		simprr	$⊢ ((x \in ℝ^{} \land x \leq B) \land (x \in ℝ^{} \land B \leq x)) \to B \leq x$
13		simplr	$⊢ ((x \in ℝ^{} \land x \leq B) \land (x \in ℝ^{} \land B \leq x)) \to x \leq B$
14	11 12 13	3jca	$⊢ ((x \in ℝ^{} \land x \leq B) \land (x \in ℝ^{} \land B \leq x)) \to (x \in ℝ^{*} \land B \leq x \land x \leq B)$
15	10 14	syl6	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to ((x \in (A, B] \land x \in [B, C)) \to (x \in ℝ^{} \land B \leq x \land x \leq B))$
16		elicc1	$⊢ (B \in ℝ^{} \land B \in ℝ^{}) \to (x \in [B, B] \leftrightarrow (x \in ℝ^{*} \land B \leq x \land x \leq B))$
17	16	anidms	$⊢ B \in ℝ^{} \to (x \in [B, B] \leftrightarrow (x \in ℝ^{} \land B \leq x \land x \leq B))$
18	17	3ad2ant2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [B, B] \leftrightarrow (x \in ℝ^{} \land B \leq x \land x \leq B))$
19	15 18	sylibrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((x \in (A, B] \land x \in [B, C)) \to x \in [B, B])$
20	19	ss2abdv	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to \{x \| (x \in (A, B] \land x \in [B, C))\} \subseteq \{x \| x \in [B, B]\}$
21	1 20	eqsstrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A, B] \cap [B, C) \subseteq \{x \| x \in [B, B]\}$
22		abid2	$⊢ \{x \| x \in [B, B]\} = [B, B]$
23	21 22	sseqtrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A, B] \cap [B, C) \subseteq [B, B]$
24	23	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to (A, B] \cap [B, C) \subseteq [B, B]$
25		iccid	$⊢ B \in ℝ^{*} \to [B, B] = \{B\}$
26	25	3ad2ant2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to [B, B] = \{B\}$
27	26	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to [B, B] = \{B\}$
28	24 27	sseqtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to (A, B] \cap [B, C) \subseteq \{B\}$
29		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A < B \land B < C)) \to B \in ℝ^{}$
30		simprl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to A < B$
31	29	xrleidd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B \leq B$
32		elioc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B \in (A, B] \leftrightarrow (B \in ℝ^{*} \land A < B \land B \leq B))$
33	32	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (B \in (A, B] \leftrightarrow (B \in ℝ^{} \land A < B \land B \leq B))$
34	33	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A < B \land B < C)) \to (B \in (A, B] \leftrightarrow (B \in ℝ^{} \land A < B \land B \leq B))$
35	29 30 31 34	mpbir3and	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B \in (A, B]$
36		simprr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B < C$
37		elico1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (B \in [B, C) \leftrightarrow (B \in ℝ^{*} \land B \leq B \land B < C))$
38	37	3adant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (B \in [B, C) \leftrightarrow (B \in ℝ^{} \land B \leq B \land B < C))$
39	38	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A < B \land B < C)) \to (B \in [B, C) \leftrightarrow (B \in ℝ^{} \land B \leq B \land B < C))$
40	29 31 36 39	mpbir3and	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B \in [B, C)$
41	35 40	elind	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B \in ((A, B] \cap [B, C))$
42	41	snssd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to \{B\} \subseteq (A, B] \cap [B, C)$
43	28 42	eqssd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to (A, B] \cap [B, C) = \{B\}$

Metamath Proof Explorer

Theorem iocinico

Proof