| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssidd 4003 |
. 2
β’ (π β π β π« π β π« π) |
| 2 | | pwidg 4624 |
. . 3
β’ (π β π β π β π« π) |
| 3 | | difss 4130 |
. . . . . 6
β’ (π β π₯) β π |
| 4 | | elpw2g 5348 |
. . . . . 6
β’ (π β π β ((π β π₯) β π« π β (π β π₯) β π)) |
| 5 | 3, 4 | mpbiri 257 |
. . . . 5
β’ (π β π β (π β π₯) β π« π) |
| 6 | 5 | a1d 25 |
. . . 4
β’ (π β π β (π₯ β π« π β (π β π₯) β π« π)) |
| 7 | 6 | ralrimiv 3141 |
. . 3
β’ (π β π β βπ₯ β π« π(π β π₯) β π« π) |
| 8 | | sspwuni 5105 |
. . . . . . . 8
β’ (π₯ β π« π β βͺ π₯
β π) |
| 9 | | vuniex 7748 |
. . . . . . . . 9
β’ βͺ π₯
β V |
| 10 | 9 | elpw 4608 |
. . . . . . . 8
β’ (βͺ π₯
β π« π β
βͺ π₯ β π) |
| 11 | 8, 10 | bitr4i 277 |
. . . . . . 7
β’ (π₯ β π« π β βͺ π₯
β π« π) |
| 12 | 11 | biimpi 215 |
. . . . . 6
β’ (π₯ β π« π β βͺ π₯
β π« π) |
| 13 | 12 | a1d 25 |
. . . . 5
β’ (π₯ β π« π β (π₯ βΌ Ο β βͺ π₯
β π« π)) |
| 14 | | elpwi 4611 |
. . . . . 6
β’ (π₯ β π« π«
π β π₯ β π« π) |
| 15 | 14 | imim1i 63 |
. . . . 5
β’ ((π₯ β π« π β (π₯ βΌ Ο β βͺ π₯
β π« π)) β
(π₯ β π«
π« π β (π₯ βΌ Ο β βͺ π₯
β π« π))) |
| 16 | 13, 15 | mp1i 13 |
. . . 4
β’ (π β π β (π₯ β π« π« π β (π₯ βΌ Ο β βͺ π₯
β π« π))) |
| 17 | 16 | ralrimiv 3141 |
. . 3
β’ (π β π β βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π)) |
| 18 | 2, 7, 17 | 3jca 1125 |
. 2
β’ (π β π β (π β π« π β§ βπ₯ β π« π(π β π₯) β π« π β§ βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π))) |
| 19 | | pwexg 5380 |
. . 3
β’ (π β π β π« π β V) |
| 20 | | issiga 33736 |
. . 3
β’
(π« π β
V β (π« π
β (sigAlgebraβπ)
β (π« π β
π« π β§ (π β π« π β§ βπ₯ β π« π(π β π₯) β π« π β§ βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π))))) |
| 21 | 19, 20 | syl 17 |
. 2
β’ (π β π β (π« π β (sigAlgebraβπ) β (π« π β π« π β§ (π β π« π β§ βπ₯ β π« π(π β π₯) β π« π β§ βπ₯ β π« π« π(π₯ βΌ Ο β βͺ π₯
β π« π))))) |
| 22 | 1, 18, 21 | mpbir2and 711 |
1
β’ (π β π β π« π β (sigAlgebraβπ)) |
