Step | Hyp | Ref
| Expression |
1 | | sepnsepolem2.1 |
. 2
β’ (π β π½ β Top) |
2 | | id 22 |
. . . . . 6
β’ (π½ β Top β π½ β Top) |
3 | 2 | sepnsepolem2 47041 |
. . . . 5
β’ (π½ β Top β (βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
β βπ¦ β π½ (π· β π¦ β§ (π₯ β© π¦) = β
))) |
4 | 3 | anbi2d 630 |
. . . 4
β’ (π½ β Top β ((πΆ β π₯ β§ βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
) β (πΆ β π₯ β§ βπ¦ β π½ (π· β π¦ β§ (π₯ β© π¦) = β
)))) |
5 | 4 | rexbidv 3172 |
. . 3
β’ (π½ β Top β (βπ₯ β π½ (πΆ β π₯ β§ βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
) β βπ₯ β π½ (πΆ β π₯ β§ βπ¦ β π½ (π· β π¦ β§ (π₯ β© π¦) = β
)))) |
6 | | ssrin 4194 |
. . . . . . 7
β’ (π§ β π₯ β (π§ β© π¦) β (π₯ β© π¦)) |
7 | | sseq0 4360 |
. . . . . . . 8
β’ (((π§ β© π¦) β (π₯ β© π¦) β§ (π₯ β© π¦) = β
) β (π§ β© π¦) = β
) |
8 | 7 | ex 414 |
. . . . . . 7
β’ ((π§ β© π¦) β (π₯ β© π¦) β ((π₯ β© π¦) = β
β (π§ β© π¦) = β
)) |
9 | 6, 8 | syl 17 |
. . . . . 6
β’ (π§ β π₯ β ((π₯ β© π¦) = β
β (π§ β© π¦) = β
)) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π½ β Top β§ π§ β π₯) β ((π₯ β© π¦) = β
β (π§ β© π¦) = β
)) |
11 | 10 | reximdv 3164 |
. . . 4
β’ ((π½ β Top β§ π§ β π₯) β (βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
β βπ¦ β ((neiβπ½)βπ·)(π§ β© π¦) = β
)) |
12 | | simpr 486 |
. . . . . . 7
β’ ((π½ β Top β§ π₯ = π§) β π₯ = π§) |
13 | 12 | ineq1d 4172 |
. . . . . 6
β’ ((π½ β Top β§ π₯ = π§) β (π₯ β© π¦) = (π§ β© π¦)) |
14 | 13 | eqeq1d 2735 |
. . . . 5
β’ ((π½ β Top β§ π₯ = π§) β ((π₯ β© π¦) = β
β (π§ β© π¦) = β
)) |
15 | 14 | rexbidv 3172 |
. . . 4
β’ ((π½ β Top β§ π₯ = π§) β (βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
β βπ¦ β ((neiβπ½)βπ·)(π§ β© π¦) = β
)) |
16 | 2, 11, 15 | opnneieqv 47029 |
. . 3
β’ (π½ β Top β (βπ₯ β ((neiβπ½)βπΆ)βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
β βπ₯ β π½ (πΆ β π₯ β§ βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
))) |
17 | | sepnsepolem1 47040 |
. . . 4
β’
(βπ₯ β
π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β
) β βπ₯ β π½ (πΆ β π₯ β§ βπ¦ β π½ (π· β π¦ β§ (π₯ β© π¦) = β
))) |
18 | 17 | a1i 11 |
. . 3
β’ (π½ β Top β (βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β
) β βπ₯ β π½ (πΆ β π₯ β§ βπ¦ β π½ (π· β π¦ β§ (π₯ β© π¦) = β
)))) |
19 | 5, 16, 18 | 3bitr4d 311 |
. 2
β’ (π½ β Top β (βπ₯ β ((neiβπ½)βπΆ)βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β
))) |
20 | 1, 19 | syl 17 |
1
β’ (π β (βπ₯ β ((neiβπ½)βπΆ)βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β
β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β
))) |