Step | Hyp | Ref
| Expression |
1 | | vex 3452 |
. . . 4
β’ π₯ β V |
2 | | vex 3452 |
. . . 4
β’ π β V |
3 | | fvex 6860 |
. . . . 5
β’ (π»β(cardβπ₯)) β V |
4 | | fvex 6860 |
. . . . 5
β’ (π·ββ© {π§
β Ο β£ Β¬ (π·βπ§) β π₯}) β V |
5 | 3, 4 | ifex 4541 |
. . . 4
β’ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) β V |
6 | | pwfseqlem4.f |
. . . . 5
β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
7 | 6 | ovmpt4g 7507 |
. . . 4
β’ ((π₯ β V β§ π β V β§ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) β V) β (π₯πΉπ) = if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
8 | 1, 2, 5, 7 | mp3an 1462 |
. . 3
β’ (π₯πΉπ) = if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) |
9 | | pwfseqlem4.ps |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) |
10 | 9 | simprbi 498 |
. . . . . . 7
β’ (π β Ο βΌ π₯) |
11 | 10 | adantl 483 |
. . . . . 6
β’ ((π β§ π) β Ο βΌ π₯) |
12 | | domnsym 9050 |
. . . . . 6
β’ (Ο
βΌ π₯ β Β¬
π₯ βΊ
Ο) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ ((π β§ π) β Β¬ π₯ βΊ Ο) |
14 | | isfinite 9595 |
. . . . 5
β’ (π₯ β Fin β π₯ βΊ
Ο) |
15 | 13, 14 | sylnibr 329 |
. . . 4
β’ ((π β§ π) β Β¬ π₯ β Fin) |
16 | 15 | iffalsed 4502 |
. . 3
β’ ((π β§ π) β if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) = (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) |
17 | 8, 16 | eqtrid 2789 |
. 2
β’ ((π β§ π) β (π₯πΉπ) = (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) |
18 | | pwfseqlem4.g |
. . . . . . 7
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) |
19 | | pwfseqlem4.x |
. . . . . . 7
β’ (π β π β π΄) |
20 | | pwfseqlem4.h |
. . . . . . 7
β’ (π β π»:Οβ1-1-ontoβπ) |
21 | | pwfseqlem4.k |
. . . . . . 7
β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) |
22 | | pwfseqlem4.d |
. . . . . . 7
β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) |
23 | 18, 19, 20, 9, 21, 22 | pwfseqlem1 10601 |
. . . . . 6
β’ ((π β§ π) β π· β (βͺ
π β Ο (π΄ βm π) β βͺ π β Ο (π₯ βm π))) |
24 | | eldif 3925 |
. . . . . 6
β’ (π· β (βͺ π β Ο (π΄ βm π) β βͺ
π β Ο (π₯ βm π)) β (π· β βͺ
π β Ο (π΄ βm π) β§ Β¬ π· β βͺ
π β Ο (π₯ βm π))) |
25 | 23, 24 | sylib 217 |
. . . . 5
β’ ((π β§ π) β (π· β βͺ
π β Ο (π΄ βm π) β§ Β¬ π· β βͺ
π β Ο (π₯ βm π))) |
26 | 25 | simpld 496 |
. . . 4
β’ ((π β§ π) β π· β βͺ
π β Ο (π΄ βm π)) |
27 | | eliun 4963 |
. . . 4
β’ (π· β βͺ π β Ο (π΄ βm π) β βπ β Ο π· β (π΄ βm π)) |
28 | 26, 27 | sylib 217 |
. . 3
β’ ((π β§ π) β βπ β Ο π· β (π΄ βm π)) |
29 | | elmapi 8794 |
. . . . . 6
β’ (π· β (π΄ βm π) β π·:πβΆπ΄) |
30 | 29 | ad2antll 728 |
. . . . 5
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β π·:πβΆπ΄) |
31 | | ssiun2 5012 |
. . . . . . . . 9
β’ (π β Ο β (π₯ βm π) β βͺ π β Ο (π₯ βm π)) |
32 | 31 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π₯ βm π) β βͺ
π β Ο (π₯ βm π)) |
33 | 25 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π) β Β¬ π· β βͺ
π β Ο (π₯ βm π)) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β Β¬ π· β βͺ
π β Ο (π₯ βm π)) |
35 | 32, 34 | ssneldd 3952 |
. . . . . . 7
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β Β¬ π· β (π₯ βm π)) |
36 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
37 | 1, 36 | elmap 8816 |
. . . . . . . 8
β’ (π· β (π₯ βm π) β π·:πβΆπ₯) |
38 | | ffn 6673 |
. . . . . . . . 9
β’ (π·:πβΆπ΄ β π· Fn π) |
39 | | ffnfv 7071 |
. . . . . . . . . 10
β’ (π·:πβΆπ₯ β (π· Fn π β§ βπ§ β π (π·βπ§) β π₯)) |
40 | 39 | baib 537 |
. . . . . . . . 9
β’ (π· Fn π β (π·:πβΆπ₯ β βπ§ β π (π·βπ§) β π₯)) |
41 | 30, 38, 40 | 3syl 18 |
. . . . . . . 8
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π·:πβΆπ₯ β βπ§ β π (π·βπ§) β π₯)) |
42 | 37, 41 | bitrid 283 |
. . . . . . 7
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π· β (π₯ βm π) β βπ§ β π (π·βπ§) β π₯)) |
43 | 35, 42 | mtbid 324 |
. . . . . 6
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β Β¬ βπ§ β π (π·βπ§) β π₯) |
44 | | nnon 7813 |
. . . . . . . . 9
β’ (π β Ο β π β On) |
45 | 44 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β π β On) |
46 | | ssrab2 4042 |
. . . . . . . . . 10
β’ {π§ β Ο β£ Β¬
(π·βπ§) β π₯} β Ο |
47 | | omsson 7811 |
. . . . . . . . . 10
β’ Ο
β On |
48 | 46, 47 | sstri 3958 |
. . . . . . . . 9
β’ {π§ β Ο β£ Β¬
(π·βπ§) β π₯} β On |
49 | | ordom 7817 |
. . . . . . . . . . . . 13
β’ Ord
Ο |
50 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β π β Ο) |
51 | | ordelss 6338 |
. . . . . . . . . . . . 13
β’ ((Ord
Ο β§ π β
Ο) β π β
Ο) |
52 | 49, 50, 51 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β π β Ο) |
53 | | rexnal 3104 |
. . . . . . . . . . . . 13
β’
(βπ§ β
π Β¬ (π·βπ§) β π₯ β Β¬ βπ§ β π (π·βπ§) β π₯) |
54 | 43, 53 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β βπ§ β π Β¬ (π·βπ§) β π₯) |
55 | | ssrexv 4016 |
. . . . . . . . . . . 12
β’ (π β Ο β
(βπ§ β π Β¬ (π·βπ§) β π₯ β βπ§ β Ο Β¬ (π·βπ§) β π₯)) |
56 | 52, 54, 55 | sylc 65 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β βπ§ β Ο Β¬ (π·βπ§) β π₯) |
57 | | rabn0 4350 |
. . . . . . . . . . 11
β’ ({π§ β Ο β£ Β¬
(π·βπ§) β π₯} β β
β βπ§ β Ο Β¬ (π·βπ§) β π₯) |
58 | 56, 57 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β {π§ β Ο β£ Β¬ (π·βπ§) β π₯} β β
) |
59 | | onint 7730 |
. . . . . . . . . 10
β’ (({π§ β Ο β£ Β¬
(π·βπ§) β π₯} β On β§ {π§ β Ο β£ Β¬ (π·βπ§) β π₯} β β
) β β© {π§
β Ο β£ Β¬ (π·βπ§) β π₯} β {π§ β Ο β£ Β¬ (π·βπ§) β π₯}) |
60 | 48, 58, 59 | sylancr 588 |
. . . . . . . . 9
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β {π§ β Ο β£ Β¬ (π·βπ§) β π₯}) |
61 | 48, 60 | sselid 3947 |
. . . . . . . 8
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β On) |
62 | | ontri1 6356 |
. . . . . . . 8
β’ ((π β On β§ β© {π§
β Ο β£ Β¬ (π·βπ§) β π₯} β On) β (π β β© {π§ β Ο β£ Β¬
(π·βπ§) β π₯} β Β¬ β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β π)) |
63 | 45, 61, 62 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π β β© {π§ β Ο β£ Β¬
(π·βπ§) β π₯} β Β¬ β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β π)) |
64 | | ssintrab 4937 |
. . . . . . . 8
β’ (π β β© {π§
β Ο β£ Β¬ (π·βπ§) β π₯} β βπ§ β Ο (Β¬ (π·βπ§) β π₯ β π β π§)) |
65 | | nnon 7813 |
. . . . . . . . . . . . . . . 16
β’ (π§ β Ο β π§ β On) |
66 | | ontri1 6356 |
. . . . . . . . . . . . . . . 16
β’ ((π β On β§ π§ β On) β (π β π§ β Β¬ π§ β π)) |
67 | 44, 65, 66 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ π§ β Ο) β (π β π§ β Β¬ π§ β π)) |
68 | 67 | imbi2d 341 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ π§ β Ο) β ((Β¬
(π·βπ§) β π₯ β π β π§) β (Β¬ (π·βπ§) β π₯ β Β¬ π§ β π))) |
69 | | con34b 316 |
. . . . . . . . . . . . . 14
β’ ((π§ β π β (π·βπ§) β π₯) β (Β¬ (π·βπ§) β π₯ β Β¬ π§ β π)) |
70 | 68, 69 | bitr4di 289 |
. . . . . . . . . . . . 13
β’ ((π β Ο β§ π§ β Ο) β ((Β¬
(π·βπ§) β π₯ β π β π§) β (π§ β π β (π·βπ§) β π₯))) |
71 | 70 | pm5.74da 803 |
. . . . . . . . . . . 12
β’ (π β Ο β ((π§ β Ο β (Β¬
(π·βπ§) β π₯ β π β π§)) β (π§ β Ο β (π§ β π β (π·βπ§) β π₯)))) |
72 | | bi2.04 389 |
. . . . . . . . . . . 12
β’ ((π§ β Ο β (π§ β π β (π·βπ§) β π₯)) β (π§ β π β (π§ β Ο β (π·βπ§) β π₯))) |
73 | 71, 72 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π β Ο β ((π§ β Ο β (Β¬
(π·βπ§) β π₯ β π β π§)) β (π§ β π β (π§ β Ο β (π·βπ§) β π₯)))) |
74 | | elnn 7818 |
. . . . . . . . . . . . . 14
β’ ((π§ β π β§ π β Ο) β π§ β Ο) |
75 | | pm2.27 42 |
. . . . . . . . . . . . . 14
β’ (π§ β Ο β ((π§ β Ο β (π·βπ§) β π₯) β (π·βπ§) β π₯)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π§ β π β§ π β Ο) β ((π§ β Ο β (π·βπ§) β π₯) β (π·βπ§) β π₯)) |
77 | 76 | expcom 415 |
. . . . . . . . . . . 12
β’ (π β Ο β (π§ β π β ((π§ β Ο β (π·βπ§) β π₯) β (π·βπ§) β π₯))) |
78 | 77 | a2d 29 |
. . . . . . . . . . 11
β’ (π β Ο β ((π§ β π β (π§ β Ο β (π·βπ§) β π₯)) β (π§ β π β (π·βπ§) β π₯))) |
79 | 73, 78 | sylbid 239 |
. . . . . . . . . 10
β’ (π β Ο β ((π§ β Ο β (Β¬
(π·βπ§) β π₯ β π β π§)) β (π§ β π β (π·βπ§) β π₯))) |
80 | 79 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β ((π§ β Ο β (Β¬ (π·βπ§) β π₯ β π β π§)) β (π§ β π β (π·βπ§) β π₯))) |
81 | 80 | ralimdv2 3161 |
. . . . . . . 8
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (βπ§ β Ο (Β¬ (π·βπ§) β π₯ β π β π§) β βπ§ β π (π·βπ§) β π₯)) |
82 | 64, 81 | biimtrid 241 |
. . . . . . 7
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π β β© {π§ β Ο β£ Β¬
(π·βπ§) β π₯} β βπ§ β π (π·βπ§) β π₯)) |
83 | 63, 82 | sylbird 260 |
. . . . . 6
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (Β¬ β© {π§
β Ο β£ Β¬ (π·βπ§) β π₯} β π β βπ§ β π (π·βπ§) β π₯)) |
84 | 43, 83 | mt3d 148 |
. . . . 5
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β π) |
85 | 30, 84 | ffvelcdmd 7041 |
. . . 4
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β π΄) |
86 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β (π·βπ¦) = (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) |
87 | 86 | eleq1d 2823 |
. . . . . . . 8
β’ (π¦ = β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β ((π·βπ¦) β π₯ β (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β π₯)) |
88 | 87 | notbid 318 |
. . . . . . 7
β’ (π¦ = β©
{π§ β Ο β£
Β¬ (π·βπ§) β π₯} β (Β¬ (π·βπ¦) β π₯ β Β¬ (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β π₯)) |
89 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π§ = π¦ β (π·βπ§) = (π·βπ¦)) |
90 | 89 | eleq1d 2823 |
. . . . . . . . 9
β’ (π§ = π¦ β ((π·βπ§) β π₯ β (π·βπ¦) β π₯)) |
91 | 90 | notbid 318 |
. . . . . . . 8
β’ (π§ = π¦ β (Β¬ (π·βπ§) β π₯ β Β¬ (π·βπ¦) β π₯)) |
92 | 91 | cbvrabv 3420 |
. . . . . . 7
β’ {π§ β Ο β£ Β¬
(π·βπ§) β π₯} = {π¦ β Ο β£ Β¬ (π·βπ¦) β π₯} |
93 | 88, 92 | elrab2 3653 |
. . . . . 6
β’ (β© {π§
β Ο β£ Β¬ (π·βπ§) β π₯} β {π§ β Ο β£ Β¬ (π·βπ§) β π₯} β (β© {π§ β Ο β£ Β¬
(π·βπ§) β π₯} β Ο β§ Β¬ (π·ββ© {π§
β Ο β£ Β¬ (π·βπ§) β π₯}) β π₯)) |
94 | 93 | simprbi 498 |
. . . . 5
β’ (β© {π§
β Ο β£ Β¬ (π·βπ§) β π₯} β {π§ β Ο β£ Β¬ (π·βπ§) β π₯} β Β¬ (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β π₯) |
95 | 60, 94 | syl 17 |
. . . 4
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β Β¬ (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β π₯) |
96 | 85, 95 | eldifd 3926 |
. . 3
β’ (((π β§ π) β§ (π β Ο β§ π· β (π΄ βm π))) β (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β (π΄ β π₯)) |
97 | 28, 96 | rexlimddv 3159 |
. 2
β’ ((π β§ π) β (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}) β (π΄ β π₯)) |
98 | 17, 97 | eqeltrd 2838 |
1
β’ ((π β§ π) β (π₯πΉπ) β (π΄ β π₯)) |