Proof of Theorem ixxss12
| Step | Hyp | Ref
| Expression |
| 1 | | ixxss12.2 |
. . . . . . . 8
⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) |
| 2 | 1 | elixx3g 13400 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐶𝑃𝐷) ↔ ((𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) ∧ (𝐶𝑇𝑤 ∧ 𝑤𝑈𝐷))) |
| 3 | 2 | simplbi 497 |
. . . . . 6
⊢ (𝑤 ∈ (𝐶𝑃𝐷) → (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝑤 ∈
ℝ*)) |
| 4 | 3 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*
∧ 𝑤 ∈
ℝ*)) |
| 5 | 4 | simp3d 1145 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤 ∈ ℝ*) |
| 6 | | simplrl 777 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐴𝑊𝐶) |
| 7 | 2 | simprbi 496 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐶𝑃𝐷) → (𝐶𝑇𝑤 ∧ 𝑤𝑈𝐷)) |
| 8 | 7 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → (𝐶𝑇𝑤 ∧ 𝑤𝑈𝐷)) |
| 9 | 8 | simpld 494 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐶𝑇𝑤) |
| 10 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐴 ∈
ℝ*) |
| 11 | 4 | simp1d 1143 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐶 ∈
ℝ*) |
| 12 | | ixxss12.3 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑤
∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤)) |
| 13 | 10, 11, 5, 12 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤)) |
| 14 | 6, 9, 13 | mp2and 699 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐴𝑅𝑤) |
| 15 | 8 | simprd 495 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤𝑈𝐷) |
| 16 | | simplrr 778 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐷𝑋𝐵) |
| 17 | 4 | simp2d 1144 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐷 ∈
ℝ*) |
| 18 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐵 ∈
ℝ*) |
| 19 | | ixxss12.4 |
. . . . . 6
⊢ ((𝑤 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) |
| 20 | 5, 17, 18, 19 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) |
| 21 | 15, 16, 20 | mp2and 699 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤𝑆𝐵) |
| 22 | | ixx.1 |
. . . . . 6
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) |
| 23 | 22 | elixx1 13396 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))) |
| 24 | 23 | ad2antrr 726 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))) |
| 25 | 5, 14, 21, 24 | mpbir3and 1343 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤 ∈ (𝐴𝑂𝐵)) |
| 26 | 25 | ex 412 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝑤 ∈ (𝐶𝑃𝐷) → 𝑤 ∈ (𝐴𝑂𝐵))) |
| 27 | 26 | ssrdv 3989 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) |