Step | Hyp | Ref
| Expression |
1 | | inex1g 5281 |
. . 3
β’ (π β βͺ ran sigAlgebra β (π β© π« π΄) β V) |
2 | 1 | adantr 482 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β (π β© π« π΄) β V) |
3 | | inss2 4194 |
. . 3
β’ (π β© π« π΄) β π« π΄ |
4 | 3 | a1i 11 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β (π β© π« π΄) β π« π΄) |
5 | | simpr 486 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β π΄ β π) |
6 | | pwidg 4585 |
. . . . 5
β’ (π΄ β π β π΄ β π« π΄) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β π΄ β π« π΄) |
8 | 5, 7 | elind 4159 |
. . 3
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β π΄ β (π β© π« π΄)) |
9 | | simpll 766 |
. . . . . 6
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β π β βͺ ran
sigAlgebra) |
10 | | simplr 768 |
. . . . . 6
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β π΄ β π) |
11 | | inss1 4193 |
. . . . . . 7
β’ (π β© π« π΄) β π |
12 | | simpr 486 |
. . . . . . 7
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β π₯ β (π β© π« π΄)) |
13 | 11, 12 | sselid 3947 |
. . . . . 6
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β π₯ β π) |
14 | | difelsiga 32772 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π β§ π₯ β π) β (π΄ β π₯) β π) |
15 | 9, 10, 13, 14 | syl3anc 1372 |
. . . . 5
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β (π΄ β π₯) β π) |
16 | | difss 4096 |
. . . . . . 7
β’ (π΄ β π₯) β π΄ |
17 | | elpwg 4568 |
. . . . . . 7
β’ ((π΄ β π₯) β π β ((π΄ β π₯) β π« π΄ β (π΄ β π₯) β π΄)) |
18 | 16, 17 | mpbiri 258 |
. . . . . 6
β’ ((π΄ β π₯) β π β (π΄ β π₯) β π« π΄) |
19 | 15, 18 | syl 17 |
. . . . 5
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β (π΄ β π₯) β π« π΄) |
20 | 15, 19 | elind 4159 |
. . . 4
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β (π β© π« π΄)) β (π΄ β π₯) β (π β© π« π΄)) |
21 | 20 | ralrimiva 3144 |
. . 3
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β βπ₯ β (π β© π« π΄)(π΄ β π₯) β (π β© π« π΄)) |
22 | | simplll 774 |
. . . . . . 7
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β π β βͺ ran
sigAlgebra) |
23 | | simplr 768 |
. . . . . . . 8
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β π₯ β π« (π β© π« π΄)) |
24 | | elpwi 4572 |
. . . . . . . . 9
β’ (π₯ β π« (π β© π« π΄) β π₯ β (π β© π« π΄)) |
25 | | sstr 3957 |
. . . . . . . . . 10
β’ ((π₯ β (π β© π« π΄) β§ (π β© π« π΄) β π) β π₯ β π) |
26 | 11, 25 | mpan2 690 |
. . . . . . . . 9
β’ (π₯ β (π β© π« π΄) β π₯ β π) |
27 | 23, 24, 26 | 3syl 18 |
. . . . . . . 8
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β π₯ β π) |
28 | | elpwg 4568 |
. . . . . . . . 9
β’ (π₯ β π« (π β© π« π΄) β (π₯ β π« π β π₯ β π)) |
29 | 28 | biimpar 479 |
. . . . . . . 8
β’ ((π₯ β π« (π β© π« π΄) β§ π₯ β π) β π₯ β π« π) |
30 | 23, 27, 29 | syl2anc 585 |
. . . . . . 7
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β π₯ β π« π) |
31 | | simpr 486 |
. . . . . . 7
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β π₯ βΌ Ο) |
32 | | sigaclcu 32756 |
. . . . . . 7
β’ ((π β βͺ ran sigAlgebra β§ π₯ β π« π β§ π₯ βΌ Ο) β βͺ π₯
β π) |
33 | 22, 30, 31, 32 | syl3anc 1372 |
. . . . . 6
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β βͺ π₯
β π) |
34 | | sstr 3957 |
. . . . . . . . 9
β’ ((π₯ β (π β© π« π΄) β§ (π β© π« π΄) β π« π΄) β π₯ β π« π΄) |
35 | 3, 34 | mpan2 690 |
. . . . . . . 8
β’ (π₯ β (π β© π« π΄) β π₯ β π« π΄) |
36 | 23, 24, 35 | 3syl 18 |
. . . . . . 7
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β π₯ β π« π΄) |
37 | | sspwuni 5065 |
. . . . . . . 8
β’ (π₯ β π« π΄ β βͺ π₯
β π΄) |
38 | | vuniex 7681 |
. . . . . . . . 9
β’ βͺ π₯
β V |
39 | 38 | elpw 4569 |
. . . . . . . 8
β’ (βͺ π₯
β π« π΄ β
βͺ π₯ β π΄) |
40 | 37, 39 | bitr4i 278 |
. . . . . . 7
β’ (π₯ β π« π΄ β βͺ π₯
β π« π΄) |
41 | 36, 40 | sylib 217 |
. . . . . 6
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β βͺ π₯
β π« π΄) |
42 | 33, 41 | elind 4159 |
. . . . 5
β’ ((((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β§ π₯ βΌ Ο) β βͺ π₯
β (π β© π«
π΄)) |
43 | 42 | ex 414 |
. . . 4
β’ (((π β βͺ ran sigAlgebra β§ π΄ β π) β§ π₯ β π« (π β© π« π΄)) β (π₯ βΌ Ο β βͺ π₯
β (π β© π«
π΄))) |
44 | 43 | ralrimiva 3144 |
. . 3
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β βπ₯ β π« (π β© π« π΄)(π₯ βΌ Ο β βͺ π₯
β (π β© π«
π΄))) |
45 | 8, 21, 44 | 3jca 1129 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β (π΄ β (π β© π« π΄) β§ βπ₯ β (π β© π« π΄)(π΄ β π₯) β (π β© π« π΄) β§ βπ₯ β π« (π β© π« π΄)(π₯ βΌ Ο β βͺ π₯
β (π β© π«
π΄)))) |
46 | | issiga 32751 |
. . 3
β’ ((π β© π« π΄) β V β ((π β© π« π΄) β (sigAlgebraβπ΄) β ((π β© π« π΄) β π« π΄ β§ (π΄ β (π β© π« π΄) β§ βπ₯ β (π β© π« π΄)(π΄ β π₯) β (π β© π« π΄) β§ βπ₯ β π« (π β© π« π΄)(π₯ βΌ Ο β βͺ π₯
β (π β© π«
π΄)))))) |
47 | 46 | biimpar 479 |
. 2
β’ (((π β© π« π΄) β V β§ ((π β© π« π΄) β π« π΄ β§ (π΄ β (π β© π« π΄) β§ βπ₯ β (π β© π« π΄)(π΄ β π₯) β (π β© π« π΄) β§ βπ₯ β π« (π β© π« π΄)(π₯ βΌ Ο β βͺ π₯
β (π β© π«
π΄))))) β (π β© π« π΄) β (sigAlgebraβπ΄)) |
48 | 2, 4, 45, 47 | syl12anc 836 |
1
β’ ((π β βͺ ran sigAlgebra β§ π΄ β π) β (π β© π« π΄) β (sigAlgebraβπ΄)) |