Step | Hyp | Ref
| Expression |
1 | | sigasspw 32779 |
. . . . 5
β’ (π‘ β (sigAlgebraβπ) β π‘ β π« π) |
2 | | velpw 4569 |
. . . . 5
β’ (π‘ β π« π«
π β π‘ β π« π) |
3 | 1, 2 | sylibr 233 |
. . . 4
β’ (π‘ β (sigAlgebraβπ) β π‘ β π« π« π) |
4 | | elrnsiga 32789 |
. . . . . 6
β’ (π‘ β (sigAlgebraβπ) β π‘ β βͺ ran
sigAlgebra) |
5 | | 0elsiga 32777 |
. . . . . 6
β’ (π‘ β βͺ ran sigAlgebra β β
β π‘) |
6 | 4, 5 | syl 17 |
. . . . 5
β’ (π‘ β (sigAlgebraβπ) β β
β π‘) |
7 | 4 | adantr 482 |
. . . . . . 7
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β π‘) β π‘ β βͺ ran
sigAlgebra) |
8 | | baselsiga 32778 |
. . . . . . . 8
β’ (π‘ β (sigAlgebraβπ) β π β π‘) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β π‘) β π β π‘) |
10 | | simpr 486 |
. . . . . . 7
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β π‘) β π₯ β π‘) |
11 | | difelsiga 32796 |
. . . . . . 7
β’ ((π‘ β βͺ ran sigAlgebra β§ π β π‘ β§ π₯ β π‘) β (π β π₯) β π‘) |
12 | 7, 9, 10, 11 | syl3anc 1372 |
. . . . . 6
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β π‘) β (π β π₯) β π‘) |
13 | 12 | ralrimiva 3140 |
. . . . 5
β’ (π‘ β (sigAlgebraβπ) β βπ₯ β π‘ (π β π₯) β π‘) |
14 | 4 | ad2antrr 725 |
. . . . . . . 8
β’ (((π‘ β (sigAlgebraβπ) β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π‘ β βͺ ran
sigAlgebra) |
15 | | simplr 768 |
. . . . . . . 8
β’ (((π‘ β (sigAlgebraβπ) β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π₯ β π« π‘) |
16 | | simprl 770 |
. . . . . . . 8
β’ (((π‘ β (sigAlgebraβπ) β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π₯ βΌ Ο) |
17 | | sigaclcu 32780 |
. . . . . . . 8
β’ ((π‘ β βͺ ran sigAlgebra β§ π₯ β π« π‘ β§ π₯ βΌ Ο) β βͺ π₯
β π‘) |
18 | 14, 15, 16, 17 | syl3anc 1372 |
. . . . . . 7
β’ (((π‘ β (sigAlgebraβπ) β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βͺ π₯ β π‘) |
19 | 18 | ex 414 |
. . . . . 6
β’ ((π‘ β (sigAlgebraβπ) β§ π₯ β π« π‘) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
20 | 19 | ralrimiva 3140 |
. . . . 5
β’ (π‘ β (sigAlgebraβπ) β βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
21 | 6, 13, 20 | 3jca 1129 |
. . . 4
β’ (π‘ β (sigAlgebraβπ) β (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘))) |
22 | 3, 21 | jca 513 |
. . 3
β’ (π‘ β (sigAlgebraβπ) β (π‘ β π« π« π β§ (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)))) |
23 | | isldsys.l |
. . . 4
β’ πΏ = {π β π« π« π β£ (β
β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} |
24 | 23 | isldsys 32819 |
. . 3
β’ (π‘ β πΏ β (π‘ β π« π« π β§ (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)))) |
25 | 22, 24 | sylibr 233 |
. 2
β’ (π‘ β (sigAlgebraβπ) β π‘ β πΏ) |
26 | 25 | ssriv 3952 |
1
β’
(sigAlgebraβπ)
β πΏ |