Step | Hyp | Ref
| Expression |
1 | | clscld.1 |
. . . 4
β’ π = βͺ
π½ |
2 | 1 | ntrval 13613 |
. . 3
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) = βͺ (π½ β© π« π)) |
3 | 2 | eqeq1d 2186 |
. 2
β’ ((π½ β Top β§ π β π) β (((intβπ½)βπ) = β
β βͺ (π½
β© π« π) =
β
)) |
4 | | notm0 3444 |
. . . 4
β’ (Β¬
βπ¦ π¦ β βͺ (π½ β© π« π) β βͺ (π½
β© π« π) =
β
) |
5 | | ancom 266 |
. . . . . . . . . 10
β’ ((π¦ β π₯ β§ π₯ β (π½ β© π« π)) β (π₯ β (π½ β© π« π) β§ π¦ β π₯)) |
6 | | elin 3319 |
. . . . . . . . . . 11
β’ (π₯ β (π½ β© π« π) β (π₯ β π½ β§ π₯ β π« π)) |
7 | 6 | anbi1i 458 |
. . . . . . . . . 10
β’ ((π₯ β (π½ β© π« π) β§ π¦ β π₯) β ((π₯ β π½ β§ π₯ β π« π) β§ π¦ β π₯)) |
8 | | anass 401 |
. . . . . . . . . 10
β’ (((π₯ β π½ β§ π₯ β π« π) β§ π¦ β π₯) β (π₯ β π½ β§ (π₯ β π« π β§ π¦ β π₯))) |
9 | 5, 7, 8 | 3bitri 206 |
. . . . . . . . 9
β’ ((π¦ β π₯ β§ π₯ β (π½ β© π« π)) β (π₯ β π½ β§ (π₯ β π« π β§ π¦ β π₯))) |
10 | 9 | exbii 1605 |
. . . . . . . 8
β’
(βπ₯(π¦ β π₯ β§ π₯ β (π½ β© π« π)) β βπ₯(π₯ β π½ β§ (π₯ β π« π β§ π¦ β π₯))) |
11 | | eluni 3813 |
. . . . . . . 8
β’ (π¦ β βͺ (π½
β© π« π) β
βπ₯(π¦ β π₯ β§ π₯ β (π½ β© π« π))) |
12 | | df-rex 2461 |
. . . . . . . 8
β’
(βπ₯ β
π½ (π₯ β π« π β§ π¦ β π₯) β βπ₯(π₯ β π½ β§ (π₯ β π« π β§ π¦ β π₯))) |
13 | 10, 11, 12 | 3bitr4i 212 |
. . . . . . 7
β’ (π¦ β βͺ (π½
β© π« π) β
βπ₯ β π½ (π₯ β π« π β§ π¦ β π₯)) |
14 | 13 | exbii 1605 |
. . . . . 6
β’
(βπ¦ π¦ β βͺ (π½
β© π« π) β
βπ¦βπ₯ β π½ (π₯ β π« π β§ π¦ β π₯)) |
15 | | rexcom4 2761 |
. . . . . 6
β’
(βπ₯ β
π½ βπ¦(π₯ β π« π β§ π¦ β π₯) β βπ¦βπ₯ β π½ (π₯ β π« π β§ π¦ β π₯)) |
16 | | 19.42v 1906 |
. . . . . . 7
β’
(βπ¦(π₯ β π« π β§ π¦ β π₯) β (π₯ β π« π β§ βπ¦ π¦ β π₯)) |
17 | 16 | rexbii 2484 |
. . . . . 6
β’
(βπ₯ β
π½ βπ¦(π₯ β π« π β§ π¦ β π₯) β βπ₯ β π½ (π₯ β π« π β§ βπ¦ π¦ β π₯)) |
18 | 14, 15, 17 | 3bitr2i 208 |
. . . . 5
β’
(βπ¦ π¦ β βͺ (π½
β© π« π) β
βπ₯ β π½ (π₯ β π« π β§ βπ¦ π¦ β π₯)) |
19 | 18 | notbii 668 |
. . . 4
β’ (Β¬
βπ¦ π¦ β βͺ (π½ β© π« π) β Β¬ βπ₯ β π½ (π₯ β π« π β§ βπ¦ π¦ β π₯)) |
20 | 4, 19 | bitr3i 186 |
. . 3
β’ (βͺ (π½
β© π« π) =
β
β Β¬ βπ₯ β π½ (π₯ β π« π β§ βπ¦ π¦ β π₯)) |
21 | | ralinexa 2504 |
. . 3
β’
(βπ₯ β
π½ (π₯ β π« π β Β¬ βπ¦ π¦ β π₯) β Β¬ βπ₯ β π½ (π₯ β π« π β§ βπ¦ π¦ β π₯)) |
22 | | velpw 3583 |
. . . . 5
β’ (π₯ β π« π β π₯ β π) |
23 | | notm0 3444 |
. . . . 5
β’ (Β¬
βπ¦ π¦ β π₯ β π₯ = β
) |
24 | 22, 23 | imbi12i 239 |
. . . 4
β’ ((π₯ β π« π β Β¬ βπ¦ π¦ β π₯) β (π₯ β π β π₯ = β
)) |
25 | 24 | ralbii 2483 |
. . 3
β’
(βπ₯ β
π½ (π₯ β π« π β Β¬ βπ¦ π¦ β π₯) β βπ₯ β π½ (π₯ β π β π₯ = β
)) |
26 | 20, 21, 25 | 3bitr2i 208 |
. 2
β’ (βͺ (π½
β© π« π) =
β
β βπ₯
β π½ (π₯ β π β π₯ = β
)) |
27 | 3, 26 | bitrdi 196 |
1
β’ ((π½ β Top β§ π β π) β (((intβπ½)βπ) = β
β βπ₯ β π½ (π₯ β π β π₯ = β
))) |