Step | Hyp | Ref
| Expression |
1 | | isfinite 9596 |
. . 3
β’ (π β Fin β π βΊ
Ο) |
2 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β Fin) β π β Fin) |
3 | | vex 3451 |
. . . . . . 7
β’ π β V |
4 | | pwfseqlem4.g |
. . . . . . . 8
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) |
5 | | pwfseqlem4.x |
. . . . . . . 8
β’ (π β π β π΄) |
6 | | pwfseqlem4.h |
. . . . . . . 8
β’ (π β π»:Οβ1-1-ontoβπ) |
7 | | pwfseqlem4.ps |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯)) |
8 | | pwfseqlem4.k |
. . . . . . . 8
β’ ((π β§ π) β πΎ:βͺ π β Ο (π₯ βm π)β1-1βπ₯) |
9 | | pwfseqlem4.d |
. . . . . . . 8
β’ π· = (πΊβ{π€ β π₯ β£ ((β‘πΎβπ€) β ran πΊ β§ Β¬ π€ β (β‘πΊβ(β‘πΎβπ€)))}) |
10 | | pwfseqlem4.f |
. . . . . . . 8
β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
11 | 4, 5, 6, 7, 8, 9, 10 | pwfseqlem2 10603 |
. . . . . . 7
β’ ((π β Fin β§ π β V) β (ππΉπ ) = (π»β(cardβπ))) |
12 | 2, 3, 11 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β Fin) β (ππΉπ ) = (π»β(cardβπ))) |
13 | | f1of 6788 |
. . . . . . . . 9
β’ (π»:Οβ1-1-ontoβπ β π»:ΟβΆπ) |
14 | 6, 13 | syl 17 |
. . . . . . . 8
β’ (π β π»:ΟβΆπ) |
15 | 14, 5 | fssd 6690 |
. . . . . . 7
β’ (π β π»:ΟβΆπ΄) |
16 | | ficardom 9905 |
. . . . . . 7
β’ (π β Fin β
(cardβπ) β
Ο) |
17 | | ffvelcdm 7036 |
. . . . . . 7
β’ ((π»:ΟβΆπ΄ β§ (cardβπ) β Ο) β (π»β(cardβπ)) β π΄) |
18 | 15, 16, 17 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β Fin) β (π»β(cardβπ)) β π΄) |
19 | 12, 18 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β Fin) β (ππΉπ ) β π΄) |
20 | 19 | ex 414 |
. . . 4
β’ (π β (π β Fin β (ππΉπ ) β π΄)) |
21 | 20 | adantr 482 |
. . 3
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (π β Fin β (ππΉπ ) β π΄)) |
22 | 1, 21 | biimtrrid 242 |
. 2
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (π βΊ Ο β (ππΉπ ) β π΄)) |
23 | | omelon 9590 |
. . . . 5
β’ Ο
β On |
24 | | onenon 9893 |
. . . . 5
β’ (Ο
β On β Ο β dom card) |
25 | 23, 24 | ax-mp 5 |
. . . 4
β’ Ο
β dom card |
26 | | simpr3 1197 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β π We π) |
27 | 26 | 19.8ad 2176 |
. . . . 5
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β βπ π We π) |
28 | | ween 9979 |
. . . . 5
β’ (π β dom card β
βπ π We π) |
29 | 27, 28 | sylibr 233 |
. . . 4
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β π β dom card) |
30 | | domtri2 9933 |
. . . 4
β’ ((Ο
β dom card β§ π
β dom card) β (Ο βΌ π β Β¬ π βΊ Ο)) |
31 | 25, 29, 30 | sylancr 588 |
. . 3
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (Ο βΌ π β Β¬ π βΊ Ο)) |
32 | | nfv 1918 |
. . . . . . 7
β’
β²π(π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) |
33 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
34 | | nfmpo2 7442 |
. . . . . . . . . 10
β’
β²π(π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
35 | 10, 34 | nfcxfr 2902 |
. . . . . . . . 9
β’
β²ππΉ |
36 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
37 | 33, 35, 36 | nfov 7391 |
. . . . . . . 8
β’
β²π(ππΉπ ) |
38 | 37 | nfel1 2920 |
. . . . . . 7
β’
β²π(ππΉπ ) β (π΄ β π) |
39 | 32, 38 | nfim 1900 |
. . . . . 6
β’
β²π((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ ) β (π΄ β π)) |
40 | | sseq1 3973 |
. . . . . . . . . 10
β’ (π = π β (π β (π Γ π) β π β (π Γ π))) |
41 | | weeq1 5625 |
. . . . . . . . . 10
β’ (π = π β (π We π β π We π)) |
42 | 40, 41 | 3anbi23d 1440 |
. . . . . . . . 9
β’ (π = π β ((π β π΄ β§ π β (π Γ π) β§ π We π) β (π β π΄ β§ π β (π Γ π) β§ π We π))) |
43 | 42 | anbi1d 631 |
. . . . . . . 8
β’ (π = π β (((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π) β ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π))) |
44 | 43 | anbi2d 630 |
. . . . . . 7
β’ (π = π β ((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)))) |
45 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π β (ππΉπ) = (ππΉπ )) |
46 | 45 | eleq1d 2819 |
. . . . . . 7
β’ (π = π β ((ππΉπ) β (π΄ β π) β (ππΉπ ) β (π΄ β π))) |
47 | 44, 46 | imbi12d 345 |
. . . . . 6
β’ (π = π β (((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ) β (π΄ β π)) β ((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ ) β (π΄ β π)))) |
48 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯(π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) |
49 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯π |
50 | | nfmpo1 7441 |
. . . . . . . . . . 11
β’
β²π₯(π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
51 | 10, 50 | nfcxfr 2902 |
. . . . . . . . . 10
β’
β²π₯πΉ |
52 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯π |
53 | 49, 51, 52 | nfov 7391 |
. . . . . . . . 9
β’
β²π₯(ππΉπ) |
54 | 53 | nfel1 2920 |
. . . . . . . 8
β’
β²π₯(ππΉπ) β (π΄ β π) |
55 | 48, 54 | nfim 1900 |
. . . . . . 7
β’
β²π₯((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ) β (π΄ β π)) |
56 | | sseq1 3973 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ β π΄ β π β π΄)) |
57 | | xpeq12 5662 |
. . . . . . . . . . . . . 14
β’ ((π₯ = π β§ π₯ = π) β (π₯ Γ π₯) = (π Γ π)) |
58 | 57 | anidms 568 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (π₯ Γ π₯) = (π Γ π)) |
59 | 58 | sseq2d 3980 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π β (π₯ Γ π₯) β π β (π Γ π))) |
60 | | weeq2 5626 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π We π₯ β π We π)) |
61 | 56, 59, 60 | 3anbi123d 1437 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β (π β π΄ β§ π β (π Γ π) β§ π We π))) |
62 | | breq2 5113 |
. . . . . . . . . . 11
β’ (π₯ = π β (Ο βΌ π₯ β Ο βΌ π)) |
63 | 61, 62 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π β (((π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯) β§ Ο βΌ π₯) β ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π))) |
64 | 7, 63 | bitrid 283 |
. . . . . . . . 9
β’ (π₯ = π β (π β ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π))) |
65 | 64 | anbi2d 630 |
. . . . . . . 8
β’ (π₯ = π β ((π β§ π) β (π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)))) |
66 | | oveq1 7368 |
. . . . . . . . 9
β’ (π₯ = π β (π₯πΉπ) = (ππΉπ)) |
67 | | difeq2 4080 |
. . . . . . . . 9
β’ (π₯ = π β (π΄ β π₯) = (π΄ β π)) |
68 | 66, 67 | eleq12d 2828 |
. . . . . . . 8
β’ (π₯ = π β ((π₯πΉπ) β (π΄ β π₯) β (ππΉπ) β (π΄ β π))) |
69 | 65, 68 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π β (((π β§ π) β (π₯πΉπ) β (π΄ β π₯)) β ((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ) β (π΄ β π)))) |
70 | 4, 5, 6, 7, 8, 9, 10 | pwfseqlem3 10604 |
. . . . . . 7
β’ ((π β§ π) β (π₯πΉπ) β (π΄ β π₯)) |
71 | 55, 69, 70 | chvarfv 2234 |
. . . . . 6
β’ ((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ) β (π΄ β π)) |
72 | 39, 47, 71 | chvarfv 2234 |
. . . . 5
β’ ((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ ) β (π΄ β π)) |
73 | 72 | eldifad 3926 |
. . . 4
β’ ((π β§ ((π β π΄ β§ π β (π Γ π) β§ π We π) β§ Ο βΌ π)) β (ππΉπ ) β π΄) |
74 | 73 | expr 458 |
. . 3
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (Ο βΌ π β (ππΉπ ) β π΄)) |
75 | 31, 74 | sylbird 260 |
. 2
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (Β¬ π βΊ Ο β (ππΉπ ) β π΄)) |
76 | 22, 75 | pm2.61d 179 |
1
β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (ππΉπ ) β π΄) |