| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | 
| 2 |  | df-ioo 13391 | . . . . . 6
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 3 | 2 | ixxssxr 13399 | . . . . 5
⊢ (𝐴(,)𝐵) ⊆
ℝ* | 
| 4 |  | infxrss 13381 | . . . . 5
⊢ (((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ∧ (𝐴(,)𝐵) ⊆ ℝ*) →
inf((𝐴(,)𝐵), ℝ*, < ) ≤
inf((𝐶(,)𝐷), ℝ*, <
)) | 
| 5 | 1, 3, 4 | sylancl 586 | . . . 4
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → inf((𝐴(,)𝐵), ℝ*, < ) ≤
inf((𝐶(,)𝐷), ℝ*, <
)) | 
| 6 |  | ioossioobi.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) | 
| 8 |  | ioossioobi.b | . . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 9 | 8 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) | 
| 10 |  | ioossioobi.cltd | . . . . . . . 8
⊢ (𝜑 → 𝐶 < 𝐷) | 
| 11 |  | ioossioobi.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈
ℝ*) | 
| 12 |  | ioossioobi.d | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈
ℝ*) | 
| 13 |  | ioon0 13413 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) → ((𝐶(,)𝐷) ≠ ∅ ↔ 𝐶 < 𝐷)) | 
| 14 | 11, 12, 13 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ((𝐶(,)𝐷) ≠ ∅ ↔ 𝐶 < 𝐷)) | 
| 15 | 10, 14 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → (𝐶(,)𝐷) ≠ ∅) | 
| 16 | 15 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → (𝐶(,)𝐷) ≠ ∅) | 
| 17 |  | ssn0 4404 | . . . . . 6
⊢ (((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ∧ (𝐶(,)𝐷) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅) | 
| 18 | 1, 16, 17 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ≠ ∅) | 
| 19 |  | idd 24 | . . . . . 6
⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑤 < 𝐵 → 𝑤 < 𝐵)) | 
| 20 |  | xrltle 13191 | . . . . . 6
⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵)) | 
| 21 |  | idd 24 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴 < 𝑤 → 𝐴 < 𝑤)) | 
| 22 |  | xrltle 13191 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤)) | 
| 23 | 2, 19, 20, 21, 22 | ixxlb 13409 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴(,)𝐵) ≠ ∅) → inf((𝐴(,)𝐵), ℝ*, < ) = 𝐴) | 
| 24 | 7, 9, 18, 23 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → inf((𝐴(,)𝐵), ℝ*, < ) = 𝐴) | 
| 25 | 11 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → 𝐶 ∈
ℝ*) | 
| 26 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → 𝐷 ∈
ℝ*) | 
| 27 |  | idd 24 | . . . . . 6
⊢ ((𝑤 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) → (𝑤 < 𝐷 → 𝑤 < 𝐷)) | 
| 28 |  | xrltle 13191 | . . . . . 6
⊢ ((𝑤 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) → (𝑤 < 𝐷 → 𝑤 ≤ 𝐷)) | 
| 29 |  | idd 24 | . . . . . 6
⊢ ((𝐶 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐶 < 𝑤 → 𝐶 < 𝑤)) | 
| 30 |  | xrltle 13191 | . . . . . 6
⊢ ((𝐶 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐶 < 𝑤 → 𝐶 ≤ 𝑤)) | 
| 31 | 2, 27, 28, 29, 30 | ixxlb 13409 | . . . . 5
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ (𝐶(,)𝐷) ≠ ∅) → inf((𝐶(,)𝐷), ℝ*, < ) = 𝐶) | 
| 32 | 25, 26, 16, 31 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → inf((𝐶(,)𝐷), ℝ*, < ) = 𝐶) | 
| 33 | 5, 24, 32 | 3brtr3d 5174 | . . 3
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → 𝐴 ≤ 𝐶) | 
| 34 |  | supxrss 13374 | . . . . 5
⊢ (((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ∧ (𝐴(,)𝐵) ⊆ ℝ*) →
sup((𝐶(,)𝐷), ℝ*, < ) ≤
sup((𝐴(,)𝐵), ℝ*, <
)) | 
| 35 | 1, 3, 34 | sylancl 586 | . . . 4
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → sup((𝐶(,)𝐷), ℝ*, < ) ≤
sup((𝐴(,)𝐵), ℝ*, <
)) | 
| 36 | 2, 27, 28, 29, 30 | ixxub 13408 | . . . . 5
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ (𝐶(,)𝐷) ≠ ∅) → sup((𝐶(,)𝐷), ℝ*, < ) = 𝐷) | 
| 37 | 25, 26, 16, 36 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → sup((𝐶(,)𝐷), ℝ*, < ) = 𝐷) | 
| 38 | 2, 19, 20, 21, 22 | ixxub 13408 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴(,)𝐵) ≠ ∅) → sup((𝐴(,)𝐵), ℝ*, < ) = 𝐵) | 
| 39 | 7, 9, 18, 38 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → sup((𝐴(,)𝐵), ℝ*, < ) = 𝐵) | 
| 40 | 35, 37, 39 | 3brtr3d 5174 | . . 3
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → 𝐷 ≤ 𝐵) | 
| 41 | 33, 40 | jca 511 | . 2
⊢ ((𝜑 ∧ (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) → (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) | 
| 42 | 6 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → 𝐴 ∈
ℝ*) | 
| 43 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → 𝐵 ∈
ℝ*) | 
| 44 |  | simprl 771 | . . 3
⊢ ((𝜑 ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → 𝐴 ≤ 𝐶) | 
| 45 |  | simprr 773 | . . 3
⊢ ((𝜑 ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → 𝐷 ≤ 𝐵) | 
| 46 |  | ioossioo 13481 | . . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | 
| 47 | 42, 43, 44, 45, 46 | syl22anc 839 | . 2
⊢ ((𝜑 ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | 
| 48 | 41, 47 | impbida 801 | 1
⊢ (𝜑 → ((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵))) |