Step | Hyp | Ref
| Expression |
1 | | tpnei.1 |
. . 3
β’ π = βͺ
π½ |
2 | 1 | elcls 22584 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
))) |
3 | 1 | isneip 22616 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ βπ₯ β π½ (π β π₯ β§ π₯ β π)))) |
4 | | r19.29r 3116 |
. . . . . . . . . . 11
β’
((βπ₯ β
π½ (π β π₯ β§ π₯ β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β βπ₯ β π½ ((π β π₯ β§ π₯ β π) β§ (π β π₯ β (π₯ β© π) β β
))) |
5 | | pm3.35 801 |
. . . . . . . . . . . . . . . 16
β’ ((π β π₯ β§ (π β π₯ β (π₯ β© π) β β
)) β (π₯ β© π) β β
) |
6 | | ssrin 4233 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π β (π₯ β© π) β (π β© π)) |
7 | | sseq2 4008 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β© π) = β
β ((π₯ β© π) β (π β© π) β (π₯ β© π) β β
)) |
8 | | ss0 4398 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β© π) β β
β (π₯ β© π) = β
) |
9 | 7, 8 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β© π) = β
β ((π₯ β© π) β (π β© π) β (π₯ β© π) = β
)) |
10 | 6, 9 | syl5com 31 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β ((π β© π) = β
β (π₯ β© π) = β
)) |
11 | 10 | necon3d 2961 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β ((π₯ β© π) β β
β (π β© π) β β
)) |
12 | 5, 11 | syl5com 31 |
. . . . . . . . . . . . . . 15
β’ ((π β π₯ β§ (π β π₯ β (π₯ β© π) β β
)) β (π₯ β π β (π β© π) β β
)) |
13 | 12 | ex 413 |
. . . . . . . . . . . . . 14
β’ (π β π₯ β ((π β π₯ β (π₯ β© π) β β
) β (π₯ β π β (π β© π) β β
))) |
14 | 13 | com23 86 |
. . . . . . . . . . . . 13
β’ (π β π₯ β (π₯ β π β ((π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
))) |
15 | 14 | imp31 418 |
. . . . . . . . . . . 12
β’ (((π β π₯ β§ π₯ β π) β§ (π β π₯ β (π₯ β© π) β β
)) β (π β© π) β β
) |
16 | 15 | rexlimivw 3151 |
. . . . . . . . . . 11
β’
(βπ₯ β
π½ ((π β π₯ β§ π₯ β π) β§ (π β π₯ β (π₯ β© π) β β
)) β (π β© π) β β
) |
17 | 4, 16 | syl 17 |
. . . . . . . . . 10
β’
((βπ₯ β
π½ (π β π₯ β§ π₯ β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β (π β© π) β β
) |
18 | 17 | ex 413 |
. . . . . . . . 9
β’
(βπ₯ β
π½ (π β π₯ β§ π₯ β π) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
)) |
19 | 18 | adantl 482 |
. . . . . . . 8
β’ ((π β π β§ βπ₯ β π½ (π β π₯ β§ π₯ β π)) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
)) |
20 | 3, 19 | syl6bi 252 |
. . . . . . 7
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)β{π}) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
))) |
21 | 20 | 3adant2 1131 |
. . . . . 6
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)β{π}) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β© π) β β
))) |
22 | 21 | com23 86 |
. . . . 5
β’ ((π½ β Top β§ π β π β§ π β π) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β (π β ((neiβπ½)β{π}) β (π β© π) β β
))) |
23 | 22 | imp 407 |
. . . 4
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β (π β ((neiβπ½)β{π}) β (π β© π) β β
)) |
24 | 23 | ralrimiv 3145 |
. . 3
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) β βπ β ((neiβπ½)β{π})(π β© π) β β
) |
25 | | opnneip 22630 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π₯ β π½ β§ π β π₯) β π₯ β ((neiβπ½)β{π})) |
26 | | ineq1 4205 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (π β© π) = (π₯ β© π)) |
27 | 26 | neeq1d 3000 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β ((π β© π) β β
β (π₯ β© π) β β
)) |
28 | 27 | rspccva 3611 |
. . . . . . . . . . . . 13
β’
((βπ β
((neiβπ½)β{π})(π β© π) β β
β§ π₯ β ((neiβπ½)β{π})) β (π₯ β© π) β β
) |
29 | | idd 24 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ (π½ β Top β§ π₯ β π½ β§ π β π₯) β§ π β π) β ((π₯ β© π) β β
β (π₯ β© π) β β
)) |
30 | 29 | 3exp 1119 |
. . . . . . . . . . . . . 14
β’ (π β π β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β ((π₯ β© π) β β
β (π₯ β© π) β β
)))) |
31 | 30 | com14 96 |
. . . . . . . . . . . . 13
β’ ((π₯ β© π) β β
β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β (π β π β (π₯ β© π) β β
)))) |
32 | 28, 31 | syl 17 |
. . . . . . . . . . . 12
β’
((βπ β
((neiβπ½)β{π})(π β© π) β β
β§ π₯ β ((neiβπ½)β{π})) β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β (π β π β (π₯ β© π) β β
)))) |
33 | 32 | ex 413 |
. . . . . . . . . . 11
β’
(βπ β
((neiβπ½)β{π})(π β© π) β β
β (π₯ β ((neiβπ½)β{π}) β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (π β π β (π β π β (π₯ β© π) β β
))))) |
34 | 33 | com3l 89 |
. . . . . . . . . 10
β’ (π₯ β ((neiβπ½)β{π}) β ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π β (π₯ β© π) β β
))))) |
35 | 25, 34 | mpcom 38 |
. . . . . . . . 9
β’ ((π½ β Top β§ π₯ β π½ β§ π β π₯) β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π β (π₯ β© π) β β
)))) |
36 | 35 | 3expia 1121 |
. . . . . . . 8
β’ ((π½ β Top β§ π₯ β π½) β (π β π₯ β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π β (π₯ β© π) β β
))))) |
37 | 36 | com25 99 |
. . . . . . 7
β’ ((π½ β Top β§ π₯ β π½) β (π β π β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π₯ β (π₯ β© π) β β
))))) |
38 | 37 | ex 413 |
. . . . . 6
β’ (π½ β Top β (π₯ β π½ β (π β π β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π β π β (π β π₯ β (π₯ β© π) β β
)))))) |
39 | 38 | com25 99 |
. . . . 5
β’ (π½ β Top β (π β π β (π β π β (βπ β ((neiβπ½)β{π})(π β© π) β β
β (π₯ β π½ β (π β π₯ β (π₯ β© π) β β
)))))) |
40 | 39 | 3imp1 1347 |
. . . 4
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ β ((neiβπ½)β{π})(π β© π) β β
) β (π₯ β π½ β (π β π₯ β (π₯ β© π) β β
))) |
41 | 40 | ralrimiv 3145 |
. . 3
β’ (((π½ β Top β§ π β π β§ π β π) β§ βπ β ((neiβπ½)β{π})(π β© π) β β
) β βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
)) |
42 | 24, 41 | impbida 799 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (βπ₯ β π½ (π β π₯ β (π₯ β© π) β β
) β βπ β ((neiβπ½)β{π})(π β© π) β β
)) |
43 | 2, 42 | bitrd 278 |
1
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ β ((neiβπ½)β{π})(π β© π) β β
)) |