Step | Hyp | Ref
| Expression |
1 | | tpnei.1 |
. . 3
β’ π = βͺ
π½ |
2 | 1 | elcls 22577 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
))) |
3 | 1 | isneip 22609 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ βπ₯ β π½ (π β π₯ β§ π₯ β π)))) |
4 | | r19.29r 3117 |
. . . . . . . . . . 11
β’
((βπ₯ β
π½ (π β π₯ β§ π₯ β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β βπ₯ β π½ ((π β π₯ β§ π₯ β π) β§ (π β π₯ β (π₯ β© π) β β
))) |
5 | | pm3.35 802 |
. . . . . . . . . . . . . . . 16
β’ ((π β π₯ β§ (π β π₯ β (π₯ β© π) β β
)) β (π₯ β© π) β β
) |
6 | | ssrin 4234 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π β (π₯ β© π) β (π β© π)) |
7 | | sseq2 4009 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β© π) = β
β ((π₯ β© π) β (π β© π) β (π₯ β© π) β β
)) |
8 | | ss0 4399 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β© π) β β
β (π₯ β© π) = β
) |
9 | 7, 8 | syl6bi 253 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β© π) = β
β ((π₯ β© π) β (π β© π) β (π₯ β© π) = β
)) |
10 | 6, 9 | syl5com 31 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β ((π β© π) = β
β (π₯ β© π) = β
)) |
11 | 10 | necon3d 2962 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β ((π₯ β© π) β β
β (π β© π) β β
)) |
12 | 5, 11 | syl5com 31 |
. . . . . . . . . . . . . . 15
β’ ((π β π₯ β§ (π β π₯ β (π₯ β© π) β β
)) β (π₯ β π β (π β© π) β β
)) |
13 | 12 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β π₯ β ((π β π₯ β (π₯ β© π) β β
) β (π₯ β π β (π β© π) β β
))) |
14 | 13 | com23 86 |
. . . . . . . . . . . . 13
β’ (π β π₯ β (π₯ β π β ((π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
))) |
15 | 14 | imp31 419 |
. . . . . . . . . . . 12
β’ (((π β π₯ β§ π₯ β π) β§ (π β π₯ β (π₯ β© π) β β
)) β (π β© π) β β
) |
16 | 15 | rexlimivw 3152 |
. . . . . . . . . . 11
β’
(βπ₯ β
π½ ((π β π₯ β§ π₯ β π) β§ (π β π₯ β (π₯ β© π) β β
)) β (π β© π) β β
) |
17 | 4, 16 | syl 17 |
. . . . . . . . . 10
β’
((βπ₯ β
π½ (π β π₯ β§ π₯ β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β (π β© π) β β
) |
18 | 17 | ex 414 |
. . . . . . . . 9
β’
(βπ₯ β
π½ (π β π₯ β§ π₯ β π) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
)) |
19 | 18 | adantl 483 |
. . . . . . . 8
β’ ((π β π β§ βπ₯ β π½ (π β π₯ β§ π₯ β π)) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
)) |
20 | 3, 19 | syl6bi 253 |
. . . . . . 7
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)β{π}) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
))) |
21 | 20 | 3adant2 1132 |
. . . . . 6
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)β{π}) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
))) |
22 | 21 | com23 86 |
. . . . 5
β’ ((π½ β Top β§ π β π β§ π β π) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β ((neiβπ½)β{π}) β (π β© π) β β
))) |
23 | 22 | imp 408 |
. . . 4
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β (π β ((neiβπ½)β{π}) β (π β© π) β β
)) |
24 | 23 | ralrimiv 3146 |
. . 3
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β βπ β ((neiβπ½)β{π})(π β© π) β β
) |
25 | | opnneip 22623 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π₯ β π½ β§ π β π₯) β π₯ β ((neiβπ½)β{π})) |
26 | | ineq1 4206 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (π β© π) = (π₯ β© π)) |
27 | 26 | neeq1d 3001 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β ((π β© π) β β
β (π₯ β© π) β β
)) |
28 | 27 | rspccva 3612 |
. . . . . . . . . . . . 13
β’
((βπ β
((neiβπ½)β{π})(π β© π) β β
β§ π₯ β ((neiβπ½)β{π})) β (π₯ β© π) β β
) |
29 | | idd 24 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ (π½ β Top β§ π₯ β π½ β§ π β π₯) β§ π β π) β ((π₯ β© π) β β
β (π₯ β© π) β β
)) |
30 | 29 | 3exp 1120 |
. . . . . . . . . . . . . 14
β’ (π β π β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β ((π₯ β© π) β β
β (π₯ β© π) β β
)))) |
31 | 30 | com14 96 |
. . . . . . . . . . . . 13
β’ ((π₯ β© π) β β
β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β (π β π β (π₯ β© π) β β
)))) |
32 | 28, 31 | syl 17 |
. . . . . . . . . . . 12
β’
((βπ β
((neiβπ½)β{π})(π β© π) β β
β§ π₯ β ((neiβπ½)β{π})) β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β (π β π β (π₯ β© π) β β
)))) |
33 | 32 | ex 414 |
. . . . . . . . . . 11
β’
(βπ β
((neiβπ½)β{π})(π β© π) β β
β (π₯ β ((neiβπ½)β{π}) β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β (π β π β (π₯ β© π) β β
))))) |
34 | 33 | com3l 89 |
. . . . . . . . . 10
β’ (π₯ β ((neiβπ½)β{π}) β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π β (π₯ β© π) β β
))))) |
35 | 25, 34 | mpcom 38 |
. . . . . . . . 9
β’ ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π β (π₯ β© π) β β
)))) |
36 | 35 | 3expia 1122 |
. . . . . . . 8
β’ ((π½ β Top β§ π₯ β π½) β (π β π₯ β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π β (π₯ β© π) β β
))))) |
37 | 36 | com25 99 |
. . . . . . 7
β’ ((π½ β Top β§ π₯ β π½) β (π β π β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π₯ β (π₯ β© π) β β
))))) |
38 | 37 | ex 414 |
. . . . . 6
β’ (π½ β Top β (π₯ β π½ β (π β π β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π₯ β (π₯ β© π) β β
)))))) |
39 | 38 | com25 99 |
. . . . 5
β’ (π½ β Top β (π β π β (π β π β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π₯ β π½ β (π β π₯ β (π₯ β© π) β β
)))))) |
40 | 39 | 3imp1 1348 |
. . . 4
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ β ((neiβπ½)β{π})(π β© π) β β
) β (π₯ β π½ β (π β π₯ β (π₯ β© π) β β
))) |
41 | 40 | ralrimiv 3146 |
. . 3
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ β ((neiβπ½)β{π})(π β© π) β β
) β βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) |
42 | 24, 41 | impbida 800 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β βπ β ((neiβπ½)β{π})(π β© π) β β
)) |
43 | 2, 42 | bitrd 279 |
1
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ β ((neiβπ½)β{π})(π β© π) β β
)) |