Step | Hyp | Ref
| Expression |
1 | | simprl 769 |
. . 3
β’ ((π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)) β π β Fin) |
2 | | innei 22628 |
. . . . . . . 8
β’ ((π½ β Top β§ π₯ β ((neiβπ½)βπ) β§ π¦ β ((neiβπ½)βπ)) β (π₯ β© π¦) β ((neiβπ½)βπ)) |
3 | 2 | 3expib 1122 |
. . . . . . 7
β’ (π½ β Top β ((π₯ β ((neiβπ½)βπ) β§ π¦ β ((neiβπ½)βπ)) β (π₯ β© π¦) β ((neiβπ½)βπ))) |
4 | 3 | ralrimivv 3198 |
. . . . . 6
β’ (π½ β Top β βπ₯ β ((neiβπ½)βπ)βπ¦ β ((neiβπ½)βπ)(π₯ β© π¦) β ((neiβπ½)βπ)) |
5 | | fiint 9323 |
. . . . . 6
β’
(βπ₯ β
((neiβπ½)βπ)βπ¦ β ((neiβπ½)βπ)(π₯ β© π¦) β ((neiβπ½)βπ) β βπ₯((π₯ β ((neiβπ½)βπ) β§ π₯ β β
β§ π₯ β Fin) β β© π₯
β ((neiβπ½)βπ))) |
6 | 4, 5 | sylib 217 |
. . . . 5
β’ (π½ β Top β βπ₯((π₯ β ((neiβπ½)βπ) β§ π₯ β β
β§ π₯ β Fin) β β© π₯
β ((neiβπ½)βπ))) |
7 | | sseq1 4007 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β ((neiβπ½)βπ) β π β ((neiβπ½)βπ))) |
8 | | neeq1 3003 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β β
β π β β
)) |
9 | | eleq1 2821 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β Fin β π β Fin)) |
10 | 7, 8, 9 | 3anbi123d 1436 |
. . . . . . . 8
β’ (π₯ = π β ((π₯ β ((neiβπ½)βπ) β§ π₯ β β
β§ π₯ β Fin) β (π β ((neiβπ½)βπ) β§ π β β
β§ π β Fin))) |
11 | | 3ancomb 1099 |
. . . . . . . . 9
β’ ((π β ((neiβπ½)βπ) β§ π β β
β§ π β Fin) β (π β ((neiβπ½)βπ) β§ π β Fin β§ π β β
)) |
12 | | 3anass 1095 |
. . . . . . . . 9
β’ ((π β ((neiβπ½)βπ) β§ π β Fin β§ π β β
) β (π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
))) |
13 | 11, 12 | bitri 274 |
. . . . . . . 8
β’ ((π β ((neiβπ½)βπ) β§ π β β
β§ π β Fin) β (π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
))) |
14 | 10, 13 | bitrdi 286 |
. . . . . . 7
β’ (π₯ = π β ((π₯ β ((neiβπ½)βπ) β§ π₯ β β
β§ π₯ β Fin) β (π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)))) |
15 | | inteq 4953 |
. . . . . . . 8
β’ (π₯ = π β β© π₯ = β©
π) |
16 | 15 | eleq1d 2818 |
. . . . . . 7
β’ (π₯ = π β (β© π₯ β ((neiβπ½)βπ) β β© π β ((neiβπ½)βπ))) |
17 | 14, 16 | imbi12d 344 |
. . . . . 6
β’ (π₯ = π β (((π₯ β ((neiβπ½)βπ) β§ π₯ β β
β§ π₯ β Fin) β β© π₯
β ((neiβπ½)βπ)) β ((π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)) β β© π
β ((neiβπ½)βπ)))) |
18 | 17 | spcgv 3586 |
. . . . 5
β’ (π β Fin β
(βπ₯((π₯ β ((neiβπ½)βπ) β§ π₯ β β
β§ π₯ β Fin) β β© π₯
β ((neiβπ½)βπ)) β ((π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)) β β© π
β ((neiβπ½)βπ)))) |
19 | 6, 18 | syl5 34 |
. . . 4
β’ (π β Fin β (π½ β Top β ((π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)) β β© π
β ((neiβπ½)βπ)))) |
20 | 19 | com3l 89 |
. . 3
β’ (π½ β Top β ((π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)) β (π β Fin β β© π
β ((neiβπ½)βπ)))) |
21 | 1, 20 | mpdi 45 |
. 2
β’ (π½ β Top β ((π β ((neiβπ½)βπ) β§ (π β Fin β§ π β β
)) β β© π
β ((neiβπ½)βπ))) |
22 | 21 | impl 456 |
1
β’ (((π½ β Top β§ π β ((neiβπ½)βπ)) β§ (π β Fin β§ π β β
)) β β© π
β ((neiβπ½)βπ)) |