Step | Hyp | Ref
| Expression |
1 | | funmpt 6543 |
. . . . . . 7
β’ Fun
(π β π« π β¦ if(π = π, {πΎ}, β
)) |
2 | | funiunfv 7199 |
. . . . . . 7
β’ (Fun
(π β π« π β¦ if(π = π, {πΎ}, β
)) β βͺ π β (π« π β© Fin)((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = βͺ ((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin))) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β βͺ
π β (π« π β© Fin)((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = βͺ ((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin))) |
4 | | elinel1 4159 |
. . . . . . . . . . . 12
β’ (π β (π« π β© Fin) β π β π« π) |
5 | 4 | elpwid 4573 |
. . . . . . . . . . 11
β’ (π β (π« π β© Fin) β π β π) |
6 | | elpwi 4571 |
. . . . . . . . . . 11
β’ (π β π« π β π β π) |
7 | 5, 6 | sylan9ssr 3962 |
. . . . . . . . . 10
β’ ((π β π« π β§ π β (π« π β© Fin)) β π β π) |
8 | | velpw 4569 |
. . . . . . . . . 10
β’ (π β π« π β π β π) |
9 | 7, 8 | sylibr 233 |
. . . . . . . . 9
β’ ((π β π« π β§ π β (π« π β© Fin)) β π β π« π) |
10 | 9 | adantll 713 |
. . . . . . . 8
β’
(((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β§ π β (π« π β© Fin)) β π β π« π) |
11 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π = π β (π = π β π = π)) |
12 | 11 | ifbid 4513 |
. . . . . . . . 9
β’ (π = π β if(π = π, {πΎ}, β
) = if(π = π, {πΎ}, β
)) |
13 | | eqid 2733 |
. . . . . . . . 9
β’ (π β π« π β¦ if(π = π, {πΎ}, β
)) = (π β π« π β¦ if(π = π, {πΎ}, β
)) |
14 | | snex 5392 |
. . . . . . . . . 10
β’ {πΎ} β V |
15 | | 0ex 5268 |
. . . . . . . . . 10
β’ β
β V |
16 | 14, 15 | ifex 4540 |
. . . . . . . . 9
β’ if(π = π, {πΎ}, β
) β V |
17 | 12, 13, 16 | fvmpt 6952 |
. . . . . . . 8
β’ (π β π« π β ((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = if(π = π, {πΎ}, β
)) |
18 | 10, 17 | syl 17 |
. . . . . . 7
β’
(((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β§ π β (π« π β© Fin)) β ((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = if(π = π, {πΎ}, β
)) |
19 | 18 | iuneq2dv 4982 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β βͺ
π β (π« π β© Fin)((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
)) |
20 | 3, 19 | eqtr3d 2775 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) = βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
)) |
21 | 20 | sseq1d 3979 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π β βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
) β π)) |
22 | | iunss 5009 |
. . . . 5
β’ (βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)if(π = π, {πΎ}, β
) β π) |
23 | | sseq1 3973 |
. . . . . . . . 9
β’ ({πΎ} = if(π = π, {πΎ}, β
) β ({πΎ} β π β if(π = π, {πΎ}, β
) β π)) |
24 | 23 | bibi1d 344 |
. . . . . . . 8
β’ ({πΎ} = if(π = π, {πΎ}, β
) β (({πΎ} β π β (π = π β πΎ β π)) β (if(π = π, {πΎ}, β
) β π β (π = π β πΎ β π)))) |
25 | | sseq1 3973 |
. . . . . . . . 9
β’ (β
= if(π = π, {πΎ}, β
) β (β
β π β if(π = π, {πΎ}, β
) β π)) |
26 | 25 | bibi1d 344 |
. . . . . . . 8
β’ (β
= if(π = π, {πΎ}, β
) β ((β
β π β (π = π β πΎ β π)) β (if(π = π, {πΎ}, β
) β π β (π = π β πΎ β π)))) |
27 | | snssg 4748 |
. . . . . . . . . 10
β’ (πΎ β π β (πΎ β π β {πΎ} β π)) |
28 | 27 | adantr 482 |
. . . . . . . . 9
β’ ((πΎ β π β§ π = π) β (πΎ β π β {πΎ} β π)) |
29 | | biimt 361 |
. . . . . . . . . 10
β’ (π = π β (πΎ β π β (π = π β πΎ β π))) |
30 | 29 | adantl 483 |
. . . . . . . . 9
β’ ((πΎ β π β§ π = π) β (πΎ β π β (π = π β πΎ β π))) |
31 | 28, 30 | bitr3d 281 |
. . . . . . . 8
β’ ((πΎ β π β§ π = π) β ({πΎ} β π β (π = π β πΎ β π))) |
32 | | 0ss 4360 |
. . . . . . . . . . 11
β’ β
β π |
33 | 32 | a1i 11 |
. . . . . . . . . 10
β’ (Β¬
π = π β β
β π) |
34 | | pm2.21 123 |
. . . . . . . . . 10
β’ (Β¬
π = π β (π = π β πΎ β π)) |
35 | 33, 34 | 2thd 265 |
. . . . . . . . 9
β’ (Β¬
π = π β (β
β π β (π = π β πΎ β π))) |
36 | 35 | adantl 483 |
. . . . . . . 8
β’ ((πΎ β π β§ Β¬ π = π) β (β
β π β (π = π β πΎ β π))) |
37 | 24, 26, 31, 36 | ifbothda 4528 |
. . . . . . 7
β’ (πΎ β π β (if(π = π, {πΎ}, β
) β π β (π = π β πΎ β π))) |
38 | 37 | ralbidv 3171 |
. . . . . 6
β’ (πΎ β π β (βπ β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)(π = π β πΎ β π))) |
39 | 38 | ad3antlr 730 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)(π = π β πΎ β π))) |
40 | 22, 39 | bitrid 283 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)(π = π β πΎ β π))) |
41 | | inss1 4192 |
. . . . . . . 8
β’
(π« π β©
Fin) β π« π |
42 | 6 | sspwd 4577 |
. . . . . . . 8
β’ (π β π« π β π« π β π« π) |
43 | 41, 42 | sstrid 3959 |
. . . . . . 7
β’ (π β π« π β (π« π β© Fin) β π«
π) |
44 | 43 | adantl 483 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π« π β© Fin) β π« π) |
45 | | ralss 4018 |
. . . . . 6
β’
((π« π β©
Fin) β π« π
β (βπ β
(π« π β©
Fin)(π = π β πΎ β π) β βπ β π« π(π β (π« π β© Fin) β (π = π β πΎ β π)))) |
46 | 44, 45 | syl 17 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β (π« π β© Fin)(π = π β πΎ β π) β βπ β π« π(π β (π« π β© Fin) β (π = π β πΎ β π)))) |
47 | | bi2.04 389 |
. . . . . . 7
β’ ((π β (π« π β© Fin) β (π = π β πΎ β π)) β (π = π β (π β (π« π β© Fin) β πΎ β π))) |
48 | 47 | ralbii 3093 |
. . . . . 6
β’
(βπ β
π« π(π β (π« π β© Fin) β (π = π β πΎ β π)) β βπ β π« π(π = π β (π β (π« π β© Fin) β πΎ β π))) |
49 | | elpwg 4567 |
. . . . . . . . 9
β’ (π β Fin β (π β π« π β π β π)) |
50 | 49 | biimparc 481 |
. . . . . . . 8
β’ ((π β π β§ π β Fin) β π β π« π) |
51 | 50 | ad2antlr 726 |
. . . . . . 7
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β π β π« π) |
52 | | eleq1 2822 |
. . . . . . . . 9
β’ (π = π β (π β (π« π β© Fin) β π β (π« π β© Fin))) |
53 | 52 | imbi1d 342 |
. . . . . . . 8
β’ (π = π β ((π β (π« π β© Fin) β πΎ β π) β (π β (π« π β© Fin) β πΎ β π))) |
54 | 53 | ceqsralv 3485 |
. . . . . . 7
β’ (π β π« π β (βπ β π« π(π = π β (π β (π« π β© Fin) β πΎ β π)) β (π β (π« π β© Fin) β πΎ β π))) |
55 | 51, 54 | syl 17 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β π« π(π = π β (π β (π« π β© Fin) β πΎ β π)) β (π β (π« π β© Fin) β πΎ β π))) |
56 | 48, 55 | bitrid 283 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β π« π(π β (π« π β© Fin) β (π = π β πΎ β π)) β (π β (π« π β© Fin) β πΎ β π))) |
57 | | simplrr 777 |
. . . . . . . . 9
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β π β Fin) |
58 | 57 | biantrud 533 |
. . . . . . . 8
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π β π« π β (π β π« π β§ π β Fin))) |
59 | | elin 3930 |
. . . . . . . 8
β’ (π β (π« π β© Fin) β (π β π« π β§ π β Fin)) |
60 | 58, 59 | bitr4di 289 |
. . . . . . 7
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π β π« π β π β (π« π β© Fin))) |
61 | | vex 3451 |
. . . . . . . 8
β’ π β V |
62 | 61 | elpw2 5306 |
. . . . . . 7
β’ (π β π« π β π β π) |
63 | 60, 62 | bitr3di 286 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π β (π« π β© Fin) β π β π)) |
64 | 63 | imbi1d 342 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β ((π β (π« π β© Fin) β πΎ β π) β (π β π β πΎ β π))) |
65 | 46, 56, 64 | 3bitrd 305 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β (π« π β© Fin)(π = π β πΎ β π) β (π β π β πΎ β π))) |
66 | 21, 40, 65 | 3bitrrd 306 |
. . 3
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β ((π β π β πΎ β π) β βͺ ((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π)) |
67 | 66 | rabbidva 3413 |
. 2
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {π β π« π β£ (π β π β πΎ β π)} = {π β π« π β£ βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π}) |
68 | | simpll 766 |
. . 3
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β π β π) |
69 | | snelpwi 5404 |
. . . . . . 7
β’ (πΎ β π β {πΎ} β π« π) |
70 | 69 | ad2antlr 726 |
. . . . . 6
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {πΎ} β π« π) |
71 | | 0elpw 5315 |
. . . . . 6
β’ β
β π« π |
72 | | ifcl 4535 |
. . . . . 6
β’ (({πΎ} β π« π β§ β
β π«
π) β if(π = π, {πΎ}, β
) β π« π) |
73 | 70, 71, 72 | sylancl 587 |
. . . . 5
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β if(π = π, {πΎ}, β
) β π« π) |
74 | 73 | adantr 482 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β if(π = π, {πΎ}, β
) β π« π) |
75 | 74 | fmpttd 7067 |
. . 3
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β (π β π« π β¦ if(π = π, {πΎ}, β
)):π« πβΆπ« π) |
76 | | isacs1i 17545 |
. . 3
β’ ((π β π β§ (π β π« π β¦ if(π = π, {πΎ}, β
)):π« πβΆπ« π) β {π β π« π β£ βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π} β (ACSβπ)) |
77 | 68, 75, 76 | syl2anc 585 |
. 2
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {π β π« π β£ βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π} β (ACSβπ)) |
78 | 67, 77 | eqeltrd 2834 |
1
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {π β π« π β£ (π β π β πΎ β π)} β (ACSβπ)) |