Step | Hyp | Ref
| Expression |
1 | | funmpt 6586 |
. . . . . . 7
β’ Fun
(π β π« π β¦ if(π = π, {πΎ}, β
)) |
2 | | funiunfv 7246 |
. . . . . . 7
β’ (Fun
(π β π« π β¦ if(π = π, {πΎ}, β
)) β βͺ π β (π« π β© Fin)((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = βͺ ((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin))) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β βͺ
π β (π« π β© Fin)((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = βͺ ((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin))) |
4 | | elinel1 4195 |
. . . . . . . . . . . 12
β’ (π β (π« π β© Fin) β π β π« π) |
5 | 4 | elpwid 4611 |
. . . . . . . . . . 11
β’ (π β (π« π β© Fin) β π β π) |
6 | | elpwi 4609 |
. . . . . . . . . . 11
β’ (π β π« π β π β π) |
7 | 5, 6 | sylan9ssr 3996 |
. . . . . . . . . 10
β’ ((π β π« π β§ π β (π« π β© Fin)) β π β π) |
8 | | velpw 4607 |
. . . . . . . . . 10
β’ (π β π« π β π β π) |
9 | 7, 8 | sylibr 233 |
. . . . . . . . 9
β’ ((π β π« π β§ π β (π« π β© Fin)) β π β π« π) |
10 | 9 | adantll 712 |
. . . . . . . 8
β’
(((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β§ π β (π« π β© Fin)) β π β π« π) |
11 | | eqeq1 2736 |
. . . . . . . . . 10
β’ (π = π β (π = π β π = π)) |
12 | 11 | ifbid 4551 |
. . . . . . . . 9
β’ (π = π β if(π = π, {πΎ}, β
) = if(π = π, {πΎ}, β
)) |
13 | | eqid 2732 |
. . . . . . . . 9
β’ (π β π« π β¦ if(π = π, {πΎ}, β
)) = (π β π« π β¦ if(π = π, {πΎ}, β
)) |
14 | | snex 5431 |
. . . . . . . . . 10
β’ {πΎ} β V |
15 | | 0ex 5307 |
. . . . . . . . . 10
β’ β
β V |
16 | 14, 15 | ifex 4578 |
. . . . . . . . 9
β’ if(π = π, {πΎ}, β
) β V |
17 | 12, 13, 16 | fvmpt 6998 |
. . . . . . . 8
β’ (π β π« π β ((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = if(π = π, {πΎ}, β
)) |
18 | 10, 17 | syl 17 |
. . . . . . 7
β’
(((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β§ π β (π« π β© Fin)) β ((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = if(π = π, {πΎ}, β
)) |
19 | 18 | iuneq2dv 5021 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β βͺ
π β (π« π β© Fin)((π β π« π β¦ if(π = π, {πΎ}, β
))βπ) = βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
)) |
20 | 3, 19 | eqtr3d 2774 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) = βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
)) |
21 | 20 | sseq1d 4013 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π β βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
) β π)) |
22 | | iunss 5048 |
. . . . 5
β’ (βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)if(π = π, {πΎ}, β
) β π) |
23 | | sseq1 4007 |
. . . . . . . . 9
β’ ({πΎ} = if(π = π, {πΎ}, β
) β ({πΎ} β π β if(π = π, {πΎ}, β
) β π)) |
24 | 23 | bibi1d 343 |
. . . . . . . 8
β’ ({πΎ} = if(π = π, {πΎ}, β
) β (({πΎ} β π β (π = π β πΎ β π)) β (if(π = π, {πΎ}, β
) β π β (π = π β πΎ β π)))) |
25 | | sseq1 4007 |
. . . . . . . . 9
β’ (β
= if(π = π, {πΎ}, β
) β (β
β π β if(π = π, {πΎ}, β
) β π)) |
26 | 25 | bibi1d 343 |
. . . . . . . 8
β’ (β
= if(π = π, {πΎ}, β
) β ((β
β π β (π = π β πΎ β π)) β (if(π = π, {πΎ}, β
) β π β (π = π β πΎ β π)))) |
27 | | snssg 4787 |
. . . . . . . . . 10
β’ (πΎ β π β (πΎ β π β {πΎ} β π)) |
28 | 27 | adantr 481 |
. . . . . . . . 9
β’ ((πΎ β π β§ π = π) β (πΎ β π β {πΎ} β π)) |
29 | | biimt 360 |
. . . . . . . . . 10
β’ (π = π β (πΎ β π β (π = π β πΎ β π))) |
30 | 29 | adantl 482 |
. . . . . . . . 9
β’ ((πΎ β π β§ π = π) β (πΎ β π β (π = π β πΎ β π))) |
31 | 28, 30 | bitr3d 280 |
. . . . . . . 8
β’ ((πΎ β π β§ π = π) β ({πΎ} β π β (π = π β πΎ β π))) |
32 | | 0ss 4396 |
. . . . . . . . . . 11
β’ β
β π |
33 | 32 | a1i 11 |
. . . . . . . . . 10
β’ (Β¬
π = π β β
β π) |
34 | | pm2.21 123 |
. . . . . . . . . 10
β’ (Β¬
π = π β (π = π β πΎ β π)) |
35 | 33, 34 | 2thd 264 |
. . . . . . . . 9
β’ (Β¬
π = π β (β
β π β (π = π β πΎ β π))) |
36 | 35 | adantl 482 |
. . . . . . . 8
β’ ((πΎ β π β§ Β¬ π = π) β (β
β π β (π = π β πΎ β π))) |
37 | 24, 26, 31, 36 | ifbothda 4566 |
. . . . . . 7
β’ (πΎ β π β (if(π = π, {πΎ}, β
) β π β (π = π β πΎ β π))) |
38 | 37 | ralbidv 3177 |
. . . . . 6
β’ (πΎ β π β (βπ β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)(π = π β πΎ β π))) |
39 | 38 | ad3antlr 729 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)(π = π β πΎ β π))) |
40 | 22, 39 | bitrid 282 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βͺ π β (π« π β© Fin)if(π = π, {πΎ}, β
) β π β βπ β (π« π β© Fin)(π = π β πΎ β π))) |
41 | | inss1 4228 |
. . . . . . . 8
β’
(π« π β©
Fin) β π« π |
42 | 6 | sspwd 4615 |
. . . . . . . 8
β’ (π β π« π β π« π β π« π) |
43 | 41, 42 | sstrid 3993 |
. . . . . . 7
β’ (π β π« π β (π« π β© Fin) β π«
π) |
44 | 43 | adantl 482 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π« π β© Fin) β π« π) |
45 | | ralss 4054 |
. . . . . 6
β’
((π« π β©
Fin) β π« π
β (βπ β
(π« π β©
Fin)(π = π β πΎ β π) β βπ β π« π(π β (π« π β© Fin) β (π = π β πΎ β π)))) |
46 | 44, 45 | syl 17 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β (π« π β© Fin)(π = π β πΎ β π) β βπ β π« π(π β (π« π β© Fin) β (π = π β πΎ β π)))) |
47 | | bi2.04 388 |
. . . . . . 7
β’ ((π β (π« π β© Fin) β (π = π β πΎ β π)) β (π = π β (π β (π« π β© Fin) β πΎ β π))) |
48 | 47 | ralbii 3093 |
. . . . . 6
β’
(βπ β
π« π(π β (π« π β© Fin) β (π = π β πΎ β π)) β βπ β π« π(π = π β (π β (π« π β© Fin) β πΎ β π))) |
49 | | elpwg 4605 |
. . . . . . . . 9
β’ (π β Fin β (π β π« π β π β π)) |
50 | 49 | biimparc 480 |
. . . . . . . 8
β’ ((π β π β§ π β Fin) β π β π« π) |
51 | 50 | ad2antlr 725 |
. . . . . . 7
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β π β π« π) |
52 | | eleq1 2821 |
. . . . . . . . 9
β’ (π = π β (π β (π« π β© Fin) β π β (π« π β© Fin))) |
53 | 52 | imbi1d 341 |
. . . . . . . 8
β’ (π = π β ((π β (π« π β© Fin) β πΎ β π) β (π β (π« π β© Fin) β πΎ β π))) |
54 | 53 | ceqsralv 3513 |
. . . . . . 7
β’ (π β π« π β (βπ β π« π(π = π β (π β (π« π β© Fin) β πΎ β π)) β (π β (π« π β© Fin) β πΎ β π))) |
55 | 51, 54 | syl 17 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β π« π(π = π β (π β (π« π β© Fin) β πΎ β π)) β (π β (π« π β© Fin) β πΎ β π))) |
56 | 48, 55 | bitrid 282 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β π« π(π β (π« π β© Fin) β (π = π β πΎ β π)) β (π β (π« π β© Fin) β πΎ β π))) |
57 | | simplrr 776 |
. . . . . . . . 9
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β π β Fin) |
58 | 57 | biantrud 532 |
. . . . . . . 8
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π β π« π β (π β π« π β§ π β Fin))) |
59 | | elin 3964 |
. . . . . . . 8
β’ (π β (π« π β© Fin) β (π β π« π β§ π β Fin)) |
60 | 58, 59 | bitr4di 288 |
. . . . . . 7
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π β π« π β π β (π« π β© Fin))) |
61 | | vex 3478 |
. . . . . . . 8
β’ π β V |
62 | 61 | elpw2 5345 |
. . . . . . 7
β’ (π β π« π β π β π) |
63 | 60, 62 | bitr3di 285 |
. . . . . 6
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (π β (π« π β© Fin) β π β π)) |
64 | 63 | imbi1d 341 |
. . . . 5
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β ((π β (π« π β© Fin) β πΎ β π) β (π β π β πΎ β π))) |
65 | 46, 56, 64 | 3bitrd 304 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β (βπ β (π« π β© Fin)(π = π β πΎ β π) β (π β π β πΎ β π))) |
66 | 21, 40, 65 | 3bitrrd 305 |
. . 3
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β ((π β π β πΎ β π) β βͺ ((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π)) |
67 | 66 | rabbidva 3439 |
. 2
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {π β π« π β£ (π β π β πΎ β π)} = {π β π« π β£ βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π}) |
68 | | simpll 765 |
. . 3
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β π β π) |
69 | | snelpwi 5443 |
. . . . . . 7
β’ (πΎ β π β {πΎ} β π« π) |
70 | 69 | ad2antlr 725 |
. . . . . 6
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {πΎ} β π« π) |
71 | | 0elpw 5354 |
. . . . . 6
β’ β
β π« π |
72 | | ifcl 4573 |
. . . . . 6
β’ (({πΎ} β π« π β§ β
β π«
π) β if(π = π, {πΎ}, β
) β π« π) |
73 | 70, 71, 72 | sylancl 586 |
. . . . 5
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β if(π = π, {πΎ}, β
) β π« π) |
74 | 73 | adantr 481 |
. . . 4
β’ ((((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β§ π β π« π) β if(π = π, {πΎ}, β
) β π« π) |
75 | 74 | fmpttd 7114 |
. . 3
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β (π β π« π β¦ if(π = π, {πΎ}, β
)):π« πβΆπ« π) |
76 | | isacs1i 17600 |
. . 3
β’ ((π β π β§ (π β π« π β¦ if(π = π, {πΎ}, β
)):π« πβΆπ« π) β {π β π« π β£ βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π} β (ACSβπ)) |
77 | 68, 75, 76 | syl2anc 584 |
. 2
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {π β π« π β£ βͺ
((π β π« π β¦ if(π = π, {πΎ}, β
)) β (π« π β© Fin)) β π} β (ACSβπ)) |
78 | 67, 77 | eqeltrd 2833 |
1
β’ (((π β π β§ πΎ β π) β§ (π β π β§ π β Fin)) β {π β π« π β£ (π β π β πΎ β π)} β (ACSβπ)) |