Step | Hyp | Ref
| Expression |
1 | | neifval.1 |
. . . . 5
β’ π = βͺ
π½ |
2 | 1 | isnei 22606 |
. . . 4
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)βπ) β (π β π β§ βπ£ β π½ (π β π£ β§ π£ β π)))) |
3 | 2 | 3adant3 1132 |
. . 3
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)βπ) β (π β π β§ βπ£ β π½ (π β π£ β§ π£ β π)))) |
4 | 3 | 3anibar 1329 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)βπ) β βπ£ β π½ (π β π£ β§ π£ β π))) |
5 | | simprrl 779 |
. . . . 5
β’ (((π½ β Top β§ π β π β§ π β π) β§ (π£ β π½ β§ (π β π£ β§ π£ β π))) β π β π£) |
6 | 1 | ssntr 22561 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ (π£ β π½ β§ π£ β π)) β π£ β ((intβπ½)βπ)) |
7 | 6 | 3adantl2 1167 |
. . . . . 6
β’ (((π½ β Top β§ π β π β§ π β π) β§ (π£ β π½ β§ π£ β π)) β π£ β ((intβπ½)βπ)) |
8 | 7 | adantrrl 722 |
. . . . 5
β’ (((π½ β Top β§ π β π β§ π β π) β§ (π£ β π½ β§ (π β π£ β§ π£ β π))) β π£ β ((intβπ½)βπ)) |
9 | 5, 8 | sstrd 3992 |
. . . 4
β’ (((π½ β Top β§ π β π β§ π β π) β§ (π£ β π½ β§ (π β π£ β§ π£ β π))) β π β ((intβπ½)βπ)) |
10 | 9 | rexlimdvaa 3156 |
. . 3
β’ ((π½ β Top β§ π β π β§ π β π) β (βπ£ β π½ (π β π£ β§ π£ β π) β π β ((intβπ½)βπ))) |
11 | | simpl1 1191 |
. . . . . 6
β’ (((π½ β Top β§ π β π β§ π β π) β§ π β ((intβπ½)βπ)) β π½ β Top) |
12 | | simpl3 1193 |
. . . . . 6
β’ (((π½ β Top β§ π β π β§ π β π) β§ π β ((intβπ½)βπ)) β π β π) |
13 | 1 | ntropn 22552 |
. . . . . 6
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π½) |
14 | 11, 12, 13 | syl2anc 584 |
. . . . 5
β’ (((π½ β Top β§ π β π β§ π β π) β§ π β ((intβπ½)βπ)) β ((intβπ½)βπ) β π½) |
15 | | simpr 485 |
. . . . 5
β’ (((π½ β Top β§ π β π β§ π β π) β§ π β ((intβπ½)βπ)) β π β ((intβπ½)βπ)) |
16 | 1 | ntrss2 22560 |
. . . . . 6
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) |
17 | 11, 12, 16 | syl2anc 584 |
. . . . 5
β’ (((π½ β Top β§ π β π β§ π β π) β§ π β ((intβπ½)βπ)) β ((intβπ½)βπ) β π) |
18 | | sseq2 4008 |
. . . . . . 7
β’ (π£ = ((intβπ½)βπ) β (π β π£ β π β ((intβπ½)βπ))) |
19 | | sseq1 4007 |
. . . . . . 7
β’ (π£ = ((intβπ½)βπ) β (π£ β π β ((intβπ½)βπ) β π)) |
20 | 18, 19 | anbi12d 631 |
. . . . . 6
β’ (π£ = ((intβπ½)βπ) β ((π β π£ β§ π£ β π) β (π β ((intβπ½)βπ) β§ ((intβπ½)βπ) β π))) |
21 | 20 | rspcev 3612 |
. . . . 5
β’
((((intβπ½)βπ) β π½ β§ (π β ((intβπ½)βπ) β§ ((intβπ½)βπ) β π)) β βπ£ β π½ (π β π£ β§ π£ β π)) |
22 | 14, 15, 17, 21 | syl12anc 835 |
. . . 4
β’ (((π½ β Top β§ π β π β§ π β π) β§ π β ((intβπ½)βπ)) β βπ£ β π½ (π β π£ β§ π£ β π)) |
23 | 22 | ex 413 |
. . 3
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((intβπ½)βπ) β βπ£ β π½ (π β π£ β§ π£ β π))) |
24 | 10, 23 | impbid 211 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (βπ£ β π½ (π β π£ β§ π£ β π) β π β ((intβπ½)βπ))) |
25 | 4, 24 | bitrd 278 |
1
β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)βπ) β π β ((intβπ½)βπ))) |