Theorem 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	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		df-in	⊢ ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) }
2		elioc1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
3	2	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
4		3simpb	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) )
5	3 4	biimtrdi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) → ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) ) )
6		elico1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶 ) ) )
7	6	3adant1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶 ) ) )
8		3simpa	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶 ) → ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) )
9	7 8	biimtrdi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,) 𝐶 ) → ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) ) )
10	5 9	anim12d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) ∧ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) ) ) )
11		simpll	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) ∧ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ* )
12		simprr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) ∧ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) ) → 𝐵 ≤ 𝑥 )
13		simplr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) ∧ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) ) → 𝑥 ≤ 𝐵 )
14	11 12 13	3jca	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) ∧ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
15	10 14	syl6	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
16		elicc1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
17	16	anidms	⊢ ( 𝐵 ∈ ℝ* → ( 𝑥 ∈ ( 𝐵 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
18	17	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
19	15 18	sylibrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → 𝑥 ∈ ( 𝐵 [,] 𝐵 ) ) )
20	19	ss2abdv	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) } ⊆ { 𝑥 ∣ 𝑥 ∈ ( 𝐵 [,] 𝐵 ) } )
21	1 20	eqsstrid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ⊆ { 𝑥 ∣ 𝑥 ∈ ( 𝐵 [,] 𝐵 ) } )
22		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ ( 𝐵 [,] 𝐵 ) } = ( 𝐵 [,] 𝐵 )
23	21 22	sseqtrdi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ⊆ ( 𝐵 [,] 𝐵 ) )
24	23	adantr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ⊆ ( 𝐵 [,] 𝐵 ) )
25		iccid	⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
26	25	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
27	26	adantr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
28	24 27	sseqtrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ⊆ { 𝐵 } )
29		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ℝ* )
30		simprl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐴 < 𝐵 )
31	29	xrleidd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ≤ 𝐵 )
32		elioc1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
33	32	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
34	33	adantr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐵 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
35	29 30 31 34	mpbir3and	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ( 𝐴 (,] 𝐵 ) )
36		simprr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 < 𝐶 )
37		elico1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐵 ∧ 𝐵 < 𝐶 ) ) )
38	37	3adant1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐵 ∧ 𝐵 < 𝐶 ) ) )
39	38	adantr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐵 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐵 ∧ 𝐵 < 𝐶 ) ) )
40	29 31 36 39	mpbir3and	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ( 𝐵 [,) 𝐶 ) )
41	35 40	elind	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) )
42	41	snssd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → { 𝐵 } ⊆ ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) )
43	28 42	eqssd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = { 𝐵 } )