Step | Hyp | Ref
| Expression |
1 | | ssidd 3972 |
. 2
β’ (π β π β π« π β π« π) |
2 | | pwidg 4585 |
. . 3
β’ (π β π β π β π« π) |
3 | | difss 4096 |
. . . . . 6
β’ (π β π₯) β π |
4 | | elpw2g 5306 |
. . . . . 6
β’ (π β π β ((π β π₯) β π« π β (π β π₯) β π)) |
5 | 3, 4 | mpbiri 258 |
. . . . 5
β’ (π β π β (π β π₯) β π« π) |
6 | 5 | a1d 25 |
. . . 4
β’ (π β π β (π₯ β π« π β (π β π₯) β π« π)) |
7 | 6 | ralrimiv 3143 |
. . 3
β’ (π β π β βπ₯ β π« π(π β π₯) β π« π) |
8 | | sspwuni 5065 |
. . . . . . . 8
β’ (π₯ β π« π β βͺ π₯
β π) |
9 | | vuniex 7681 |
. . . . . . . . 9
β’ βͺ π₯
β V |
10 | 9 | elpw 4569 |
. . . . . . . 8
β’ (βͺ π₯
β π« π β
βͺ π₯ β π) |
11 | 8, 10 | bitr4i 278 |
. . . . . . 7
β’ (π₯ β π« π β βͺ π₯
β π« π) |
12 | 11 | biimpi 215 |
. . . . . 6
β’ (π₯ β π« π β βͺ π₯
β π« π) |
13 | 12 | a1d 25 |
. . . . 5
β’ (π₯ β π« π β (π₯ βΌ Ο β βͺ π₯
β π« π)) |
14 | | elpwi 4572 |
. . . . . 6
β’ (π₯ β π« π«
π β π₯ β π« π) |
15 | 14 | imim1i 63 |
. . . . 5
β’ ((π₯ β π« π β (π₯ βΌ Ο β βͺ π₯
β π« π)) β
(π₯ β π«
π« π β (π₯ βΌ Ο β βͺ π₯
β π« π))) |
16 | 13, 15 | mp1i 13 |
. . . 4
β’ (π β π β (π₯ β π« π« π β (π₯ βΌ Ο β βͺ π₯
β π« π))) |
17 | 16 | ralrimiv 3143 |
. . 3
β’ (π β π β βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π)) |
18 | 2, 7, 17 | 3jca 1129 |
. 2
β’ (π β π β (π β π« π β§ βπ₯ β π« π(π β π₯) β π« π β§ βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π))) |
19 | | pwexg 5338 |
. . 3
β’ (π β π β π« π β V) |
20 | | issiga 32751 |
. . 3
β’
(π« π β
V β (π« π
β (sigAlgebraβπ)
β (π« π β
π« π β§ (π β π« π β§ βπ₯ β π« π(π β π₯) β π« π β§ βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π))))) |
21 | 19, 20 | syl 17 |
. 2
β’ (π β π β (π« π β (sigAlgebraβπ) β (π« π β π« π β§ (π β π« π β§ βπ₯ β π« π(π β π₯) β π« π β§ βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π))))) |
22 | 1, 18, 21 | mpbir2and 712 |
1
β’ (π β π β π« π β (sigAlgebraβπ)) |