Step | Hyp | Ref
| Expression |
1 | | riotauni 7320 |
. . . . . . . . 9
β’
(β!π€ β
π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β (β©π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) = βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
2 | | riotacl 7332 |
. . . . . . . . 9
β’
(β!π€ β
π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β (β©π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β π§) |
3 | 1, 2 | eqeltrrd 2839 |
. . . . . . . 8
β’
(β!π€ β
π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β π§) |
4 | | elequ2 2122 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β (π€ β π’ β π€ β π§)) |
5 | | elequ1 2114 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β (π’ β π£ β π§ β π£)) |
6 | 5 | anbi1d 631 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β ((π’ β π£ β§ π€ β π£) β (π§ β π£ β§ π€ β π£))) |
7 | 6 | rexbidv 3176 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β (βπ£ β π¦ (π’ β π£ β§ π€ β π£) β βπ£ β π¦ (π§ β π£ β§ π€ β π£))) |
8 | 4, 7 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π’ = π§ β ((π€ β π’ β§ βπ£ β π¦ (π’ β π£ β§ π€ β π£)) β (π€ β π§ β§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)))) |
9 | 8 | rabbidva2 3410 |
. . . . . . . . . . 11
β’ (π’ = π§ β {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} = {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
10 | 9 | unieqd 4880 |
. . . . . . . . . 10
β’ (π’ = π§ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} = βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
11 | | eqid 2737 |
. . . . . . . . . 10
β’ (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) |
12 | | vex 3450 |
. . . . . . . . . . . 12
β’ π§ β V |
13 | 12 | rabex 5290 |
. . . . . . . . . . 11
β’ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β V |
14 | 13 | uniex 7679 |
. . . . . . . . . 10
β’ βͺ {π€
β π§ β£
βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β V |
15 | 10, 11, 14 | fvmpt 6949 |
. . . . . . . . 9
β’ (π§ β π₯ β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) = βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)}) |
16 | 15 | eleq1d 2823 |
. . . . . . . 8
β’ (π§ β π₯ β (((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§ β βͺ {π€ β π§ β£ βπ£ β π¦ (π§ β π£ β§ π€ β π£)} β π§)) |
17 | 3, 16 | syl5ibr 246 |
. . . . . . 7
β’ (π§ β π₯ β (β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£) β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§)) |
18 | 17 | imim2d 57 |
. . . . . 6
β’ (π§ β π₯ β ((π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§))) |
19 | 18 | ralimia 3084 |
. . . . 5
β’
(βπ§ β
π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπ§ β π₯ (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§)) |
20 | | ssrab2 4038 |
. . . . . . . . . . 11
β’ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β π’ |
21 | | elssuni 4899 |
. . . . . . . . . . 11
β’ (π’ β π₯ β π’ β βͺ π₯) |
22 | 20, 21 | sstrid 3956 |
. . . . . . . . . 10
β’ (π’ β π₯ β {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β βͺ π₯) |
23 | 22 | unissd 4876 |
. . . . . . . . 9
β’ (π’ β π₯ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β βͺ βͺ π₯) |
24 | | vex 3450 |
. . . . . . . . . . . 12
β’ π₯ β V |
25 | 24 | uniex 7679 |
. . . . . . . . . . 11
β’ βͺ π₯
β V |
26 | 25 | uniex 7679 |
. . . . . . . . . 10
β’ βͺ βͺ π₯ β V |
27 | 26 | elpw2 5303 |
. . . . . . . . 9
β’ (βͺ {π€
β π’ β£
βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β π« βͺ βͺ π₯ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β βͺ βͺ π₯) |
28 | 23, 27 | sylibr 233 |
. . . . . . . 8
β’ (π’ β π₯ β βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)} β π« βͺ βͺ π₯) |
29 | 11, 28 | fmpti 7061 |
. . . . . . 7
β’ (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}):π₯βΆπ« βͺ βͺ π₯ |
30 | 26 | pwex 5336 |
. . . . . . 7
β’ π«
βͺ βͺ π₯ β V |
31 | | fex2 7871 |
. . . . . . 7
β’ (((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}):π₯βΆπ« βͺ βͺ π₯ β§ π₯ β V β§ π« βͺ βͺ π₯ β V) β (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β V) |
32 | 29, 24, 30, 31 | mp3an 1462 |
. . . . . 6
β’ (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β V |
33 | | fveq1 6842 |
. . . . . . . . 9
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β (πβπ§) = ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§)) |
34 | 33 | eleq1d 2823 |
. . . . . . . 8
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β ((πβπ§) β π§ β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§)) |
35 | 34 | imbi2d 341 |
. . . . . . 7
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β ((π§ β β
β (πβπ§) β π§) β (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§))) |
36 | 35 | ralbidv 3175 |
. . . . . 6
β’ (π = (π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)}) β (βπ§ β π₯ (π§ β β
β (πβπ§) β π§) β βπ§ β π₯ (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§))) |
37 | 32, 36 | spcev 3566 |
. . . . 5
β’
(βπ§ β
π₯ (π§ β β
β ((π’ β π₯ β¦ βͺ {π€ β π’ β£ βπ£ β π¦ (π’ β π£ β§ π€ β π£)})βπ§) β π§) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
38 | 19, 37 | syl 17 |
. . . 4
β’
(βπ§ β
π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
39 | 38 | exlimiv 1934 |
. . 3
β’
(βπ¦βπ§ β π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
40 | 39 | alimi 1814 |
. 2
β’
(βπ₯βπ¦βπ§ β π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
41 | | dfac3 10058 |
. 2
β’
(CHOICE β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
42 | 40, 41 | sylibr 233 |
1
β’
(βπ₯βπ¦βπ§ β π₯ (π§ β β
β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β
CHOICE) |