Step | Hyp | Ref
| Expression |
1 | | pwundif 4627 |
. 2
β’ π«
(π βͺ {π₯}) = ((π« (π βͺ {π₯}) β π« π) βͺ π« π) |
2 | | vex 3477 |
. . . . . . . . 9
β’ π β V |
3 | | snex 5432 |
. . . . . . . . 9
β’ {π₯} β V |
4 | 2, 3 | unex 7736 |
. . . . . . . 8
β’ (π βͺ {π₯}) β V |
5 | | pwfilemOLD.1 |
. . . . . . . 8
β’ πΉ = (π β π« π β¦ (π βͺ {π₯})) |
6 | 4, 5 | fnmpti 6694 |
. . . . . . 7
β’ πΉ Fn π« π |
7 | | dffn4 6812 |
. . . . . . 7
β’ (πΉ Fn π« π β πΉ:π« πβontoβran πΉ) |
8 | 6, 7 | mpbi 229 |
. . . . . 6
β’ πΉ:π« πβontoβran πΉ |
9 | | fodomfi 9328 |
. . . . . 6
β’
((π« π β
Fin β§ πΉ:π« πβontoβran πΉ) β ran πΉ βΌ π« π) |
10 | 8, 9 | mpan2 688 |
. . . . 5
β’
(π« π β
Fin β ran πΉ βΌ
π« π) |
11 | | domfi 9195 |
. . . . 5
β’
((π« π β
Fin β§ ran πΉ βΌ
π« π) β ran
πΉ β
Fin) |
12 | 10, 11 | mpdan 684 |
. . . 4
β’
(π« π β
Fin β ran πΉ β
Fin) |
13 | | eldifi 4127 |
. . . . . . . . 9
β’ (π β (π« (π βͺ {π₯}) β π« π) β π β π« (π βͺ {π₯})) |
14 | 3 | elpwun 7759 |
. . . . . . . . 9
β’ (π β π« (π βͺ {π₯}) β (π β {π₯}) β π« π) |
15 | 13, 14 | sylib 217 |
. . . . . . . 8
β’ (π β (π« (π βͺ {π₯}) β π« π) β (π β {π₯}) β π« π) |
16 | | undif1 4476 |
. . . . . . . . 9
β’ ((π β {π₯}) βͺ {π₯}) = (π βͺ {π₯}) |
17 | | elpwunsn 4688 |
. . . . . . . . . . 11
β’ (π β (π« (π βͺ {π₯}) β π« π) β π₯ β π) |
18 | 17 | snssd 4813 |
. . . . . . . . . 10
β’ (π β (π« (π βͺ {π₯}) β π« π) β {π₯} β π) |
19 | | ssequn2 4184 |
. . . . . . . . . 10
β’ ({π₯} β π β (π βͺ {π₯}) = π) |
20 | 18, 19 | sylib 217 |
. . . . . . . . 9
β’ (π β (π« (π βͺ {π₯}) β π« π) β (π βͺ {π₯}) = π) |
21 | 16, 20 | eqtr2id 2784 |
. . . . . . . 8
β’ (π β (π« (π βͺ {π₯}) β π« π) β π = ((π β {π₯}) βͺ {π₯})) |
22 | | uneq1 4157 |
. . . . . . . . 9
β’ (π = (π β {π₯}) β (π βͺ {π₯}) = ((π β {π₯}) βͺ {π₯})) |
23 | 22 | rspceeqv 3634 |
. . . . . . . 8
β’ (((π β {π₯}) β π« π β§ π = ((π β {π₯}) βͺ {π₯})) β βπ β π« ππ = (π βͺ {π₯})) |
24 | 15, 21, 23 | syl2anc 583 |
. . . . . . 7
β’ (π β (π« (π βͺ {π₯}) β π« π) β βπ β π« ππ = (π βͺ {π₯})) |
25 | 5, 4 | elrnmpti 5960 |
. . . . . . 7
β’ (π β ran πΉ β βπ β π« ππ = (π βͺ {π₯})) |
26 | 24, 25 | sylibr 233 |
. . . . . 6
β’ (π β (π« (π βͺ {π₯}) β π« π) β π β ran πΉ) |
27 | 26 | ssriv 3987 |
. . . . 5
β’
(π« (π βͺ
{π₯}) β π«
π) β ran πΉ |
28 | | ssdomg 8999 |
. . . . 5
β’ (ran
πΉ β Fin β
((π« (π βͺ {π₯}) β π« π) β ran πΉ β (π« (π βͺ {π₯}) β π« π) βΌ ran πΉ)) |
29 | 12, 27, 28 | mpisyl 21 |
. . . 4
β’
(π« π β
Fin β (π« (π
βͺ {π₯}) β
π« π) βΌ ran
πΉ) |
30 | | domfi 9195 |
. . . 4
β’ ((ran
πΉ β Fin β§
(π« (π βͺ {π₯}) β π« π) βΌ ran πΉ) β (π« (π βͺ {π₯}) β π« π) β Fin) |
31 | 12, 29, 30 | syl2anc 583 |
. . 3
β’
(π« π β
Fin β (π« (π
βͺ {π₯}) β
π« π) β
Fin) |
32 | | unfi 9175 |
. . 3
β’
(((π« (π
βͺ {π₯}) β
π« π) β Fin
β§ π« π β
Fin) β ((π« (π
βͺ {π₯}) β
π« π) βͺ
π« π) β
Fin) |
33 | 31, 32 | mpancom 685 |
. 2
β’
(π« π β
Fin β ((π« (π
βͺ {π₯}) β
π« π) βͺ
π« π) β
Fin) |
34 | 1, 33 | eqeltrid 2836 |
1
β’
(π« π β
Fin β π« (π
βͺ {π₯}) β
Fin) |