Step | Hyp | Ref
| Expression |
1 | | sigasspw 32779 |
. . . . 5
β’ (π‘ β (sigAlgebraβπ) β π‘ β π« π) |
2 | | velpw 4569 |
. . . . 5
β’ (π‘ β π« π«
π β π‘ β π« π) |
3 | 1, 2 | sylibr 233 |
. . . 4
β’ (π‘ β (sigAlgebraβπ) β π‘ β π« π« π) |
4 | | elrnsiga 32789 |
. . . . . . 7
β’ (π‘ β (sigAlgebraβπ) β π‘ β βͺ ran
sigAlgebra) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β π‘ β βͺ ran sigAlgebra) |
6 | | eldifsn 4751 |
. . . . . . . . . 10
β’ (π₯ β ((π« π‘ β© Fin) β {β
})
β (π₯ β (π«
π‘ β© Fin) β§ π₯ β β
)) |
7 | 6 | biimpi 215 |
. . . . . . . . 9
β’ (π₯ β ((π« π‘ β© Fin) β {β
})
β (π₯ β (π«
π‘ β© Fin) β§ π₯ β β
)) |
8 | 7 | adantl 483 |
. . . . . . . 8
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β (π₯ β (π« π‘ β© Fin) β§ π₯ β β
)) |
9 | 8 | simpld 496 |
. . . . . . 7
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β π₯ β (π« π‘ β© Fin)) |
10 | 9 | elin1d 4162 |
. . . . . 6
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β π₯ β π« π‘) |
11 | 9 | elin2d 4163 |
. . . . . . 7
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β π₯ β Fin) |
12 | | fict 9597 |
. . . . . . 7
β’ (π₯ β Fin β π₯ βΌ
Ο) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β π₯ βΌ
Ο) |
14 | 8 | simprd 497 |
. . . . . 6
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β π₯ β β
) |
15 | | sigaclci 32795 |
. . . . . 6
β’ (((π‘ β βͺ ran sigAlgebra β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ π₯ β β
)) β β© π₯
β π‘) |
16 | 5, 10, 13, 14, 15 | syl22anc 838 |
. . . . 5
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β ((π« π‘ β© Fin) β {β
})) β β© π₯
β π‘) |
17 | 16 | ralrimiva 3140 |
. . . 4
β’ (π‘ β (sigAlgebraβπ) β βπ₯ β ((π« π‘ β© Fin) β
{β
})β© π₯ β π‘) |
18 | 3, 17 | jca 513 |
. . 3
β’ (π‘ β (sigAlgebraβπ) β (π‘ β π« π« π β§ βπ₯ β ((π« π‘ β© Fin) β {β
})β© π₯
β π‘)) |
19 | | ispisys.p |
. . . 4
β’ π = {π β π« π« π β£ (fiβπ ) β π } |
20 | 19 | ispisys2 32816 |
. . 3
β’ (π‘ β π β (π‘ β π« π« π β§ βπ₯ β ((π« π‘ β© Fin) β {β
})β© π₯
β π‘)) |
21 | 18, 20 | sylibr 233 |
. 2
β’ (π‘ β (sigAlgebraβπ) β π‘ β π) |
22 | 21 | ssriv 3952 |
1
β’
(sigAlgebraβπ)
β π |