Proof of Theorem cdleme40v
| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . . . 5
⊢ (𝑠 = 𝑢 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑢 ≤ (𝑃 ∨ 𝑄))) |
| 2 | | cdleme40.g |
. . . . . . . . . . . 12
⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) |
| 3 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑢 → (𝑠 ∨ 𝑡) = (𝑢 ∨ 𝑡)) |
| 4 | 3 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑢 → ((𝑠 ∨ 𝑡) ∧ 𝑊) = ((𝑢 ∨ 𝑡) ∧ 𝑊)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑢 → (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)) = (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))) |
| 6 | 5 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑢 → ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) |
| 7 | 2, 6 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑢 → 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) |
| 8 | 7 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑢 → (𝑦 = 𝐺 ↔ 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))))) |
| 9 | 8 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑠 = 𝑢 → (((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺) ↔ ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))))) |
| 10 | 9 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑠 = 𝑢 → (∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺) ↔ ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))))) |
| 11 | 10 | riotabidv 7390 |
. . . . . . 7
⊢ (𝑠 = 𝑢 → (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))))) |
| 12 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))) ↔ 𝑧 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))))) |
| 13 | 12 | imbi2d 340 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) ↔ ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))))) |
| 14 | 13 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) ↔ ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))))) |
| 15 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑣 → (𝑡 ≤ 𝑊 ↔ 𝑣 ≤ 𝑊)) |
| 16 | 15 | notbid 318 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑣 → (¬ 𝑡 ≤ 𝑊 ↔ ¬ 𝑣 ≤ 𝑊)) |
| 17 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑣 → (𝑡 ≤ (𝑃 ∨ 𝑄) ↔ 𝑣 ≤ (𝑃 ∨ 𝑄))) |
| 18 | 17 | notbid 318 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑣 → (¬ 𝑡 ≤ (𝑃 ∨ 𝑄) ↔ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄))) |
| 19 | 16, 18 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑣 → ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) ↔ (¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)))) |
| 20 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑣 → (𝑡 ∨ 𝑈) = (𝑣 ∨ 𝑈)) |
| 21 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑣 → (𝑃 ∨ 𝑡) = (𝑃 ∨ 𝑣)) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑣 → ((𝑃 ∨ 𝑡) ∧ 𝑊) = ((𝑃 ∨ 𝑣) ∧ 𝑊)) |
| 23 | 22 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑣 → (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑣) ∧ 𝑊))) |
| 24 | 20, 23 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑣 → ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) = ((𝑣 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑣) ∧ 𝑊)))) |
| 25 | | cdleme40.e |
. . . . . . . . . . . . . . . 16
⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) |
| 26 | | cdleme40r.t |
. . . . . . . . . . . . . . . 16
⊢ 𝑇 = ((𝑣 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑣) ∧ 𝑊))) |
| 27 | 24, 25, 26 | 3eqtr4g 2802 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑣 → 𝐸 = 𝑇) |
| 28 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑣 → (𝑢 ∨ 𝑡) = (𝑢 ∨ 𝑣)) |
| 29 | 28 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑣 → ((𝑢 ∨ 𝑡) ∧ 𝑊) = ((𝑢 ∨ 𝑣) ∧ 𝑊)) |
| 30 | 27, 29 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑣 → (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)) = (𝑇 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊))) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑣 → ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (𝑇 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊)))) |
| 32 | | cdleme40r.x |
. . . . . . . . . . . . 13
⊢ 𝑋 = ((𝑃 ∨ 𝑄) ∧ (𝑇 ∨ ((𝑢 ∨ 𝑣) ∧ 𝑊))) |
| 33 | 31, 32 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑣 → ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))) = 𝑋) |
| 34 | 33 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑣 → (𝑧 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))) ↔ 𝑧 = 𝑋)) |
| 35 | 19, 34 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑣 → (((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) ↔ ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋))) |
| 36 | 35 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) ↔ ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋)) |
| 37 | 14, 36 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊)))) ↔ ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋))) |
| 38 | 37 | cbvriotavw 7398 |
. . . . . . 7
⊢
(℩𝑦
∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑢 ∨ 𝑡) ∧ 𝑊))))) = (℩𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋)) |
| 39 | 11, 38 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑠 = 𝑢 → (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) = (℩𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋))) |
| 40 | | cdleme40.i |
. . . . . 6
⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) |
| 41 | | cdleme40r.o |
. . . . . 6
⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐴 ((¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑄)) → 𝑧 = 𝑋)) |
| 42 | 39, 40, 41 | 3eqtr4g 2802 |
. . . . 5
⊢ (𝑠 = 𝑢 → 𝐼 = 𝑂) |
| 43 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑠 = 𝑢 → (𝑠 ∨ 𝑈) = (𝑢 ∨ 𝑈)) |
| 44 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑠 = 𝑢 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑢)) |
| 45 | 44 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑠 = 𝑢 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑢) ∧ 𝑊)) |
| 46 | 45 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑠 = 𝑢 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) |
| 47 | 43, 46 | oveq12d 7449 |
. . . . . 6
⊢ (𝑠 = 𝑢 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊)))) |
| 48 | | cdleme40.d |
. . . . . 6
⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) |
| 49 | | cdleme40r.y |
. . . . . 6
⊢ 𝑌 = ((𝑢 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑢) ∧ 𝑊))) |
| 50 | 47, 48, 49 | 3eqtr4g 2802 |
. . . . 5
⊢ (𝑠 = 𝑢 → 𝐷 = 𝑌) |
| 51 | 1, 42, 50 | ifbieq12d 4554 |
. . . 4
⊢ (𝑠 = 𝑢 → if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) = if(𝑢 ≤ (𝑃 ∨ 𝑄), 𝑂, 𝑌)) |
| 52 | | cdleme40.n |
. . . 4
⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) |
| 53 | | cdleme40r.v |
. . . 4
⊢ 𝑉 = if(𝑢 ≤ (𝑃 ∨ 𝑄), 𝑂, 𝑌) |
| 54 | 51, 52, 53 | 3eqtr4g 2802 |
. . 3
⊢ (𝑠 = 𝑢 → 𝑁 = 𝑉) |
| 55 | 54 | cbvcsbv 3911 |
. 2
⊢
⦋𝑅 /
𝑠⦌𝑁 = ⦋𝑅 / 𝑢⦌𝑉 |
| 56 | 55 | a1i 11 |
1
⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = ⦋𝑅 / 𝑢⦌𝑉) |