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	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,] 𝐶 ) ∩ ( 𝐵 (,] 𝐶 ) ) = ( 𝐵 (,] 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( ( 𝐴 (,] 𝐶 ) ∩ ( 𝐵 (,] 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 (,] 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) )
2		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ^* )
3		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐶 ∈ ℝ^* )
4		elioc1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐶 ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
5	2 3 4	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐶 ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
6		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ^* )
7		elioc1	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
8	6 3 7	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
9	5 8	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 (,] 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ↔ ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) ) )
10		simp31	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝑥 ∈ ℝ^* )
11	2	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝐴 ∈ ℝ^* )
12	6	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝐵 ∈ ℝ^* )
13		simp2	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝐴 ≤ 𝐵 )
14		simp32	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝐵 < 𝑥 )
15	11 12 10 13 14	xrlelttrd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝐴 < 𝑥 )
16		simp33	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → 𝑥 ≤ 𝐶 )
17	10 15 16	3jca	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) → ( 𝑥 ∈ ℝ^* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) )
18	17	3expia	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) → ( 𝑥 ∈ ℝ^* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
19	18	pm4.71rd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ↔ ( ( 𝑥 ∈ ℝ^* ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ∧ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) ) )
20	9 19	bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 (,] 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
21	1 20	bitrid	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝑥 ∈ ( ( 𝐴 (,] 𝐶 ) ∩ ( 𝐵 (,] 𝐶 ) ) ↔ ( 𝑥 ∈ ℝ^* ∧ 𝐵 < 𝑥 ∧ 𝑥 ≤ 𝐶 ) ) )
22	21 8	bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝑥 ∈ ( ( 𝐴 (,] 𝐶 ) ∩ ( 𝐵 (,] 𝐶 ) ) ↔ 𝑥 ∈ ( 𝐵 (,] 𝐶 ) ) )
23	22	eqrdv	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,] 𝐶 ) ∩ ( 𝐵 (,] 𝐶 ) ) = ( 𝐵 (,] 𝐶 ) )

Metamath Proof Explorer

Theorem iocinioc2

Proof