Proof of Theorem ixxin
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | inrab 4316 | . . 3
⊢ ({𝑧 ∈ ℝ*
∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)} ∩ {𝑧 ∈ ℝ* ∣ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷)}) = {𝑧 ∈ ℝ* ∣ ((𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵) ∧ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷))} | 
| 2 |  | ixx.1 | . . . . 5
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) | 
| 3 | 2 | ixxval 13395 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) | 
| 4 | 2 | ixxval 13395 | . . . 4
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) → (𝐶𝑂𝐷) = {𝑧 ∈ ℝ* ∣ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷)}) | 
| 5 | 3, 4 | ineqan12d 4222 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ ((𝐴𝑂𝐵) ∩ (𝐶𝑂𝐷)) = ({𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)} ∩ {𝑧 ∈ ℝ* ∣ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷)})) | 
| 6 |  | ixxin.2 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ↔ (𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧))) | 
| 7 | 6 | ad4ant124 1174 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
∧ 𝑧 ∈
ℝ*) → (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ↔ (𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧))) | 
| 8 |  | ixxin.3 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐷
∈ ℝ*) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) | 
| 9 | 8 | 3expb 1121 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 𝐷
∈ ℝ*)) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) | 
| 10 | 9 | ancoms 458 | . . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) ∧ 𝑧 ∈ ℝ*) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) | 
| 11 | 10 | adantll 714 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
∧ 𝑧 ∈
ℝ*) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) | 
| 12 | 7, 11 | anbi12d 632 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
∧ 𝑧 ∈
ℝ*) → ((if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷)) ↔ ((𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧) ∧ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷)))) | 
| 13 |  | an4 656 | . . . . . 6
⊢ (((𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵) ∧ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷)) ↔ ((𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧) ∧ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) | 
| 14 | 12, 13 | bitr4di 289 | . . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
∧ 𝑧 ∈
ℝ*) → ((if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷)) ↔ ((𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵) ∧ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷)))) | 
| 15 | 14 | rabbidva 3443 | . . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ {𝑧 ∈
ℝ* ∣ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷))} = {𝑧 ∈ ℝ* ∣ ((𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵) ∧ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷))}) | 
| 16 | 15 | an4s 660 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ {𝑧 ∈
ℝ* ∣ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷))} = {𝑧 ∈ ℝ* ∣ ((𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵) ∧ (𝐶𝑅𝑧 ∧ 𝑧𝑆𝐷))}) | 
| 17 | 1, 5, 16 | 3eqtr4a 2803 | . 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ ((𝐴𝑂𝐵) ∩ (𝐶𝑂𝐷)) = {𝑧 ∈ ℝ* ∣ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷))}) | 
| 18 |  | ifcl 4571 | . . . . 5
⊢ ((𝐶 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → if(𝐴 ≤ 𝐶, 𝐶, 𝐴) ∈
ℝ*) | 
| 19 | 18 | ancoms 458 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → if(𝐴 ≤ 𝐶, 𝐶, 𝐴) ∈
ℝ*) | 
| 20 |  | ifcl 4571 | . . . 4
⊢ ((𝐵 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) → if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ∈
ℝ*) | 
| 21 | 2 | ixxval 13395 | . . . 4
⊢
((if(𝐴 ≤ 𝐶, 𝐶, 𝐴) ∈ ℝ* ∧ if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ∈ ℝ*) →
(if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷)) = {𝑧 ∈ ℝ* ∣ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷))}) | 
| 22 | 19, 20, 21 | syl2an 596 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷)) = {𝑧 ∈ ℝ* ∣ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷))}) | 
| 23 | 22 | an4s 660 | . 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷)) = {𝑧 ∈ ℝ* ∣ (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ∧ 𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷))}) | 
| 24 | 17, 23 | eqtr4d 2780 | 1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*))
→ ((𝐴𝑂𝐵) ∩ (𝐶𝑂𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) |