Step | Hyp | Ref
| Expression |
1 | | riotauni 7371 |
. . . . . . . . 9
β’
(β!π€ β
π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β (β©π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) = βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
2 | | riotacl 7383 |
. . . . . . . . 9
β’
(β!π€ β
π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β (β©π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β π§) |
3 | 1, 2 | eqeltrrd 2835 |
. . . . . . . 8
β’
(β!π€ β
π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β π§) |
4 | | elequ2 2122 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β (π€ β π’ β π€ β π§)) |
5 | | elequ1 2114 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β (π’ β π£ β π§ β π£)) |
6 | 5 | anbi1d 631 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β ((π’ β π£ β§ π€ β π£) β (π§ β π£ β§ π€ β π£))) |
7 | 6 | rexbidv 3179 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β (βπ£ β π¦ (π’ β π£ β§ π€ β π£) β βπ£ β π¦ (π§ β π£ β§ π€ β π£))) |
8 | 4, 7 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π’ = π§ β ((π€ β π’ β§ βπ£ β π¦ (π’ β π£ β§ π€ β π£)) β (π€ β π§ β§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)))) |
9 | 8 | rabbidva2 3435 |
. . . . . . . . . . 11
β’ (π’ = π§ β {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} = {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
10 | 9 | unieqd 4923 |
. . . . . . . . . 10
β’ (π’ = π§ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} = βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
11 | | eqid 2733 |
. . . . . . . . . 10
β’ (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) |
12 | | vex 3479 |
. . . . . . . . . . . 12
β’ π§ β V |
13 | 12 | rabex 5333 |
. . . . . . . . . . 11
β’ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β V |
14 | 13 | uniex 7731 |
. . . . . . . . . 10
β’ βͺ {π€
β π§ β£
βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β V |
15 | 10, 11, 14 | fvmpt 6999 |
. . . . . . . . 9
β’ (π§ β π₯ β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) = βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
16 | 15 | eleq1d 2819 |
. . . . . . . 8
β’ (π§ β π₯ β (((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§ β βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β π§)) |
17 | 3, 16 | imbitrrid 245 |
. . . . . . 7
β’ (π§ β π₯ β (β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§)) |
18 | 17 | imim2d 57 |
. . . . . 6
β’ (π§ β π₯ β ((π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§))) |
19 | 18 | ralimia 3081 |
. . . . 5
β’
(βπ§ β
π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπ§ β π₯ (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§)) |
20 | | ssrab2 4078 |
. . . . . . . . . . 11
β’ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β π’ |
21 | | elssuni 4942 |
. . . . . . . . . . 11
β’ (π’ β π₯ β π’ β βͺ π₯) |
22 | 20, 21 | sstrid 3994 |
. . . . . . . . . 10
β’ (π’ β π₯ β {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β βͺ π₯) |
23 | 22 | unissd 4919 |
. . . . . . . . 9
β’ (π’ β π₯ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β βͺ βͺ π₯) |
24 | | vex 3479 |
. . . . . . . . . . . 12
β’ π₯ β V |
25 | 24 | uniex 7731 |
. . . . . . . . . . 11
β’ βͺ π₯
β V |
26 | 25 | uniex 7731 |
. . . . . . . . . 10
β’ βͺ βͺ π₯ β V |
27 | 26 | elpw2 5346 |
. . . . . . . . 9
β’ (βͺ {π€
β π’ β£
βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β π« βͺ βͺ π₯ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β βͺ βͺ π₯) |
28 | 23, 27 | sylibr 233 |
. . . . . . . 8
β’ (π’ β π₯ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β π« βͺ βͺ π₯) |
29 | 11, 28 | fmpti 7112 |
. . . . . . 7
β’ (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}):π₯βΆπ« βͺ βͺ π₯ |
30 | 26 | pwex 5379 |
. . . . . . 7
β’ π«
βͺ βͺ π₯ β V |
31 | | fex2 7924 |
. . . . . . 7
β’ (((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}):π₯βΆπ« βͺ βͺ π₯ β§ π₯ β V β§ π« βͺ βͺ π₯ β V) β (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β V) |
32 | 29, 24, 30, 31 | mp3an 1462 |
. . . . . 6
β’ (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β V |
33 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β (πβπ§) = ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§)) |
34 | 33 | eleq1d 2819 |
. . . . . . . 8
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β ((πβπ§) β π§ β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§)) |
35 | 34 | imbi2d 341 |
. . . . . . 7
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β ((π§ β β
β (πβπ§) β π§) β (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§))) |
36 | 35 | ralbidv 3178 |
. . . . . 6
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β (βπ§ β π₯ (π§ β β
β (πβπ§) β π§) β βπ§ β π₯ (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§))) |
37 | 32, 36 | spcev 3597 |
. . . . 5
β’
(βπ§ β
π₯ (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
38 | 19, 37 | syl 17 |
. . . 4
β’
(βπ§ β
π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
39 | 38 | exlimiv 1934 |
. . 3
β’
(βπ¦βπ§ β π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
40 | 39 | alimi 1814 |
. 2
β’
(βπ₯βπ¦βπ§ β π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
41 | | dfac3 10116 |
. 2
β’
(CHOICE β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
42 | 40, 41 | sylibr 233 |
1
β’
(βπ₯βπ¦βπ§ β π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β
CHOICE) |