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βπ)) |