| Step | Hyp | Ref
| Expression |
|---|
| 1 | | 0elpw 5353 |
. . 3
β’ β
β π« π |
| 2 | | pwidg 4621 |
. . 3
β’ (π β π β π β π« π) |
| 3 | | prssi 4823 |
. . 3
β’ ((β
β π« π β§
π β π« π) β {β
, π} β π« π) |
| 4 | 1, 2, 3 | sylancr 587 |
. 2
β’ (π β π β {β
, π} β π« π) |
| 5 | | prid2g 4764 |
. . 3
β’ (π β π β π β {β
, π}) |
| 6 | | dif0 4371 |
. . . . 5
β’ (π β β
) = π |
| 7 | 6, 5 | eqeltrid 2837 |
. . . 4
β’ (π β π β (π β β
) β {β
, π}) |
| 8 | | difid 4369 |
. . . . 5
β’ (π β π) = β
|
| 9 | | 0ex 5306 |
. . . . . . 7
β’ β
β V |
| 10 | 9 | prid1 4765 |
. . . . . 6
β’ β
β {β
, π} |
| 11 | 10 | a1i 11 |
. . . . 5
β’ (π β π β β
β {β
, π}) |
| 12 | 8, 11 | eqeltrid 2837 |
. . . 4
β’ (π β π β (π β π) β {β
, π}) |
| 13 | | difeq2 4115 |
. . . . . . 7
β’ (π₯ = β
β (π β π₯) = (π β β
)) |
| 14 | 13 | eleq1d 2818 |
. . . . . 6
β’ (π₯ = β
β ((π β π₯) β {β
, π} β (π β β
) β {β
, π})) |
| 15 | | difeq2 4115 |
. . . . . . 7
β’ (π₯ = π β (π β π₯) = (π β π)) |
| 16 | 15 | eleq1d 2818 |
. . . . . 6
β’ (π₯ = π β ((π β π₯) β {β
, π} β (π β π) β {β
, π})) |
| 17 | 14, 16 | ralprg 4697 |
. . . . 5
β’ ((β
β V β§ π β
π) β (βπ₯ β {β
, π} (π β π₯) β {β
, π} β ((π β β
) β {β
, π} β§ (π β π) β {β
, π}))) |
| 18 | 9, 17 | mpan 688 |
. . . 4
β’ (π β π β (βπ₯ β {β
, π} (π β π₯) β {β
, π} β ((π β β
) β {β
, π} β§ (π β π) β {β
, π}))) |
| 19 | 7, 12, 18 | mpbir2and 711 |
. . 3
β’ (π β π β βπ₯ β {β
, π} (π β π₯) β {β
, π}) |
| 20 | | uni0 4938 |
. . . . . . . . 9
β’ βͺ β
= β
|
| 21 | 20, 10 | eqeltri 2829 |
. . . . . . . 8
β’ βͺ β
β {β
, π} |
| 22 | 9 | unisn 4929 |
. . . . . . . . 9
β’ βͺ {β
} = β
|
| 23 | 22, 10 | eqeltri 2829 |
. . . . . . . 8
β’ βͺ {β
} β {β
, π} |
| 24 | 21, 23 | pm3.2i 471 |
. . . . . . 7
β’ (βͺ β
β {β
, π} β§ βͺ
{β
} β {β
, π}) |
| 25 | | snex 5430 |
. . . . . . . . 9
β’ {β
}
β V |
| 26 | 9, 25 | pm3.2i 471 |
. . . . . . . 8
β’ (β
β V β§ {β
} β V) |
| 27 | | unieq 4918 |
. . . . . . . . . 10
β’ (π₯ = β
β βͺ π₯ =
βͺ β
) |
| 28 | 27 | eleq1d 2818 |
. . . . . . . . 9
β’ (π₯ = β
β (βͺ π₯
β {β
, π} β
βͺ β
β {β
, π})) |
| 29 | | unieq 4918 |
. . . . . . . . . 10
β’ (π₯ = {β
} β βͺ π₯ =
βͺ {β
}) |
| 30 | 29 | eleq1d 2818 |
. . . . . . . . 9
β’ (π₯ = {β
} β (βͺ π₯
β {β
, π} β
βͺ {β
} β {β
, π})) |
| 31 | 28, 30 | ralprg 4697 |
. . . . . . . 8
β’ ((β
β V β§ {β
} β V) β (βπ₯ β {β
, {β
}}βͺ π₯
β {β
, π} β
(βͺ β
β {β
, π} β§ βͺ
{β
} β {β
, π}))) |
| 32 | 26, 31 | mp1i 13 |
. . . . . . 7
β’ (π β π β (βπ₯ β {β
, {β
}}βͺ π₯
β {β
, π} β
(βͺ β
β {β
, π} β§ βͺ
{β
} β {β
, π}))) |
| 33 | 24, 32 | mpbiri 257 |
. . . . . 6
β’ (π β π β βπ₯ β {β
, {β
}}βͺ π₯
β {β
, π}) |
| 34 | | unisng 4928 |
. . . . . . . 8
β’ (π β π β βͺ {π} = π) |
| 35 | 34, 5 | eqeltrd 2833 |
. . . . . . 7
β’ (π β π β βͺ {π} β {β
, π}) |
| 36 | | uniprg 4924 |
. . . . . . . . . 10
β’ ((β
β V β§ π β
π) β βͺ {β
, π} = (β
βͺ π)) |
| 37 | 9, 36 | mpan 688 |
. . . . . . . . 9
β’ (π β π β βͺ
{β
, π} = (β
βͺ π)) |
| 38 | | uncom 4152 |
. . . . . . . . . 10
β’ (β
βͺ π) = (π βͺ β
) |
| 39 | | un0 4389 |
. . . . . . . . . 10
β’ (π βͺ β
) = π |
| 40 | 38, 39 | eqtri 2760 |
. . . . . . . . 9
β’ (β
βͺ π) = π |
| 41 | 37, 40 | eqtrdi 2788 |
. . . . . . . 8
β’ (π β π β βͺ
{β
, π} = π) |
| 42 | 41, 5 | eqeltrd 2833 |
. . . . . . 7
β’ (π β π β βͺ
{β
, π} β
{β
, π}) |
| 43 | | snex 5430 |
. . . . . . . . 9
β’ {π} β V |
| 44 | | prex 5431 |
. . . . . . . . 9
β’ {β
,
π} β
V |
| 45 | 43, 44 | pm3.2i 471 |
. . . . . . . 8
β’ ({π} β V β§ {β
, π} β V) |
| 46 | | unieq 4918 |
. . . . . . . . . 10
β’ (π₯ = {π} β βͺ π₯ = βͺ
{π}) |
| 47 | 46 | eleq1d 2818 |
. . . . . . . . 9
β’ (π₯ = {π} β (βͺ π₯ β {β
, π} β βͺ {π}
β {β
, π})) |
| 48 | | unieq 4918 |
. . . . . . . . . 10
β’ (π₯ = {β
, π} β βͺ π₯ = βͺ
{β
, π}) |
| 49 | 48 | eleq1d 2818 |
. . . . . . . . 9
β’ (π₯ = {β
, π} β (βͺ π₯ β {β
, π} β βͺ {β
, π} β {β
, π})) |
| 50 | 47, 49 | ralprg 4697 |
. . . . . . . 8
β’ (({π} β V β§ {β
, π} β V) β
(βπ₯ β {{π}, {β
, π}}βͺ π₯ β {β
, π} β (βͺ {π}
β {β
, π} β§
βͺ {β
, π} β {β
, π}))) |
| 51 | 45, 50 | mp1i 13 |
. . . . . . 7
β’ (π β π β (βπ₯ β {{π}, {β
, π}}βͺ π₯ β {β
, π} β (βͺ {π}
β {β
, π} β§
βͺ {β
, π} β {β
, π}))) |
| 52 | 35, 42, 51 | mpbir2and 711 |
. . . . . 6
β’ (π β π β βπ₯ β {{π}, {β
, π}}βͺ π₯ β {β
, π}) |
| 53 | | ralun 4191 |
. . . . . 6
β’
((βπ₯ β
{β
, {β
}}βͺ π₯ β {β
, π} β§ βπ₯ β {{π}, {β
, π}}βͺ π₯ β {β
, π}) β βπ₯ β ({β
, {β
}}
βͺ {{π}, {β
, π}})βͺ
π₯ β {β
, π}) |
| 54 | 33, 52, 53 | syl2anc 584 |
. . . . 5
β’ (π β π β βπ₯ β ({β
, {β
}} βͺ {{π}, {β
, π}})βͺ π₯ β {β
, π}) |
| 55 | | pwpr 4901 |
. . . . . 6
β’ π«
{β
, π} = ({β
,
{β
}} βͺ {{π},
{β
, π}}) |
| 56 | 55 | raleqi 3323 |
. . . . 5
β’
(βπ₯ β
π« {β
, π}βͺ π₯
β {β
, π} β
βπ₯ β ({β
,
{β
}} βͺ {{π},
{β
, π}})βͺ π₯
β {β
, π}) |
| 57 | 54, 56 | sylibr 233 |
. . . 4
β’ (π β π β βπ₯ β π« {β
, π}βͺ π₯ β {β
, π}) |
| 58 | | ax-1 6 |
. . . . 5
β’ (βͺ π₯
β {β
, π} β
(π₯ βΌ Ο β
βͺ π₯ β {β
, π})) |
| 59 | 58 | ralimi 3083 |
. . . 4
β’
(βπ₯ β
π« {β
, π}βͺ π₯
β {β
, π} β
βπ₯ β π«
{β
, π} (π₯ βΌ Ο β βͺ π₯
β {β
, π})) |
| 60 | 57, 59 | syl 17 |
. . 3
β’ (π β π β βπ₯ β π« {β
, π} (π₯ βΌ Ο β βͺ π₯
β {β
, π})) |
| 61 | 5, 19, 60 | 3jca 1128 |
. 2
β’ (π β π β (π β {β
, π} β§ βπ₯ β {β
, π} (π β π₯) β {β
, π} β§ βπ₯ β π« {β
, π} (π₯ βΌ Ο β βͺ π₯
β {β
, π}))) |
| 62 | | issiga 33098 |
. . 3
β’
({β
, π} β
V β ({β
, π}
β (sigAlgebraβπ)
β ({β
, π}
β π« π β§
(π β {β
, π} β§ βπ₯ β {β
, π} (π β π₯) β {β
, π} β§ βπ₯ β π« {β
, π} (π₯ βΌ Ο β βͺ π₯
β {β
, π}))))) |
| 63 | 44, 62 | ax-mp 5 |
. 2
β’
({β
, π} β
(sigAlgebraβπ) β
({β
, π} β
π« π β§ (π β {β
, π} β§ βπ₯ β {β
, π} (π β π₯) β {β
, π} β§ βπ₯ β π« {β
, π} (π₯ βΌ Ο β βͺ π₯
β {β
, π})))) |
| 64 | 4, 61, 63 | sylanbrc 583 |
1
β’ (π β π β {β
, π} β (sigAlgebraβπ)) |
