Metamath Proof Explorer

Theorem ixxin

Description: Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypotheses ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
ixxin.2 ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ z ∈ ℝ * → if A ≤ C C A R z ↔ A R z ∧ C R z
ixxin.3 ⊢ z ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * → z S if B ≤ D B D ↔ z S B ∧ z S D
Assertion ixxin ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * → A O B ∩ C O D = if A ≤ C C A O if B ≤ D B D

Proof

Step Hyp Ref Expression
1 ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
2 ixxin.2 ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ z ∈ ℝ * → if A ≤ C C A R z ↔ A R z ∧ C R z
3 ixxin.3 ⊢ z ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * → z S if B ≤ D B D ↔ z S B ∧ z S D
4 inrab ⊢ z ∈ ℝ * | A R z ∧ z S B ∩ z ∈ ℝ * | C R z ∧ z S D = z ∈ ℝ * | A R z ∧ z S B ∧ C R z ∧ z S D
5 1 ixxval ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A O B = z ∈ ℝ * | A R z ∧ z S B
6 1 ixxval ⊢ C ∈ ℝ * ∧ D ∈ ℝ * → C O D = z ∈ ℝ * | C R z ∧ z S D
7 5 6 ineqan12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * → A O B ∩ C O D = z ∈ ℝ * | A R z ∧ z S B ∩ z ∈ ℝ * | C R z ∧ z S D
8 2 ad4ant124 ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * ∧ z ∈ ℝ * → if A ≤ C C A R z ↔ A R z ∧ C R z
9 3 3expb ⊢ z ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * → z S if B ≤ D B D ↔ z S B ∧ z S D
10 9 ancoms ⊢ B ∈ ℝ * ∧ D ∈ ℝ * ∧ z ∈ ℝ * → z S if B ≤ D B D ↔ z S B ∧ z S D
11 10 adantll ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * ∧ z ∈ ℝ * → z S if B ≤ D B D ↔ z S B ∧ z S D
12 8 11 anbi12d ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * ∧ z ∈ ℝ * → if A ≤ C C A R z ∧ z S if B ≤ D B D ↔ A R z ∧ C R z ∧ z S B ∧ z S D
13 an4 ⊢ A R z ∧ z S B ∧ C R z ∧ z S D ↔ A R z ∧ C R z ∧ z S B ∧ z S D
14 12 13 bitr4di ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * ∧ z ∈ ℝ * → if A ≤ C C A R z ∧ z S if B ≤ D B D ↔ A R z ∧ z S B ∧ C R z ∧ z S D
15 14 rabbidva ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * → z ∈ ℝ * | if A ≤ C C A R z ∧ z S if B ≤ D B D = z ∈ ℝ * | A R z ∧ z S B ∧ C R z ∧ z S D
16 15 an4s ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * → z ∈ ℝ * | if A ≤ C C A R z ∧ z S if B ≤ D B D = z ∈ ℝ * | A R z ∧ z S B ∧ C R z ∧ z S D
17 4 7 16 3eqtr4a ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * → A O B ∩ C O D = z ∈ ℝ * | if A ≤ C C A R z ∧ z S if B ≤ D B D
18 ifcl ⊢ C ∈ ℝ * ∧ A ∈ ℝ * → if A ≤ C C A ∈ ℝ *
19 18 ancoms ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → if A ≤ C C A ∈ ℝ *
20 ifcl ⊢ B ∈ ℝ * ∧ D ∈ ℝ * → if B ≤ D B D ∈ ℝ *
21 1 ixxval ⊢ if A ≤ C C A ∈ ℝ * ∧ if B ≤ D B D ∈ ℝ * → if A ≤ C C A O if B ≤ D B D = z ∈ ℝ * | if A ≤ C C A R z ∧ z S if B ≤ D B D
22 19 20 21 syl2an ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * → if A ≤ C C A O if B ≤ D B D = z ∈ ℝ * | if A ≤ C C A R z ∧ z S if B ≤ D B D
23 22 an4s ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * → if A ≤ C C A O if B ≤ D B D = z ∈ ℝ * | if A ≤ C C A R z ∧ z S if B ≤ D B D
24 17 23 eqtr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * → A O B ∩ C O D = if A ≤ C C A O if B ≤ D B D