Step | Hyp | Ref
| Expression |
1 | | fin23lem33.f |
. . 3
β’ πΉ = {π β£ βπ β (π« π βm Ο)(βπ₯ β Ο (πβsuc π₯) β (πβπ₯) β β© ran
π β ran π)} |
2 | | fin23lem.f |
. . 3
β’ (π β β:Οβ1-1βV) |
3 | | fin23lem.g |
. . 3
β’ (π β βͺ ran β
β πΊ) |
4 | | fin23lem.h |
. . 3
β’ (π β βπ((π:Οβ1-1βV β§ βͺ ran π β πΊ) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β βͺ ran
π))) |
5 | | fin23lem.i |
. . 3
β’ π = (rec(π, β) βΎ Ο) |
6 | 1, 2, 3, 4, 5 | fin23lem38 10344 |
. 2
β’ (π β Β¬ β© ran (π β Ο β¦ βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ))) |
7 | 1, 2, 3, 4, 5 | fin23lem35 10342 |
. . . . . . 7
β’ ((π β§ π β Ο) β βͺ ran (πβsuc π) β βͺ ran
(πβπ)) |
8 | 7 | pssssd 4098 |
. . . . . 6
β’ ((π β§ π β Ο) β βͺ ran (πβsuc π) β βͺ ran
(πβπ)) |
9 | | peano2 7881 |
. . . . . . . . 9
β’ (π β Ο β suc π β
Ο) |
10 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = suc π β (πβπ) = (πβsuc π)) |
11 | 10 | rneqd 5938 |
. . . . . . . . . . 11
β’ (π = suc π β ran (πβπ) = ran (πβsuc π)) |
12 | 11 | unieqd 4923 |
. . . . . . . . . 10
β’ (π = suc π β βͺ ran
(πβπ) = βͺ ran (πβsuc π)) |
13 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β Ο β¦ βͺ ran (πβπ)) = (π β Ο β¦ βͺ ran (πβπ)) |
14 | | fvex 6905 |
. . . . . . . . . . . 12
β’ (πβsuc π) β V |
15 | 14 | rnex 7903 |
. . . . . . . . . . 11
β’ ran
(πβsuc π) β V |
16 | 15 | uniex 7731 |
. . . . . . . . . 10
β’ βͺ ran (πβsuc π) β V |
17 | 12, 13, 16 | fvmpt 6999 |
. . . . . . . . 9
β’ (suc
π β Ο β
((π β Ο β¦
βͺ ran (πβπ))βsuc π) = βͺ ran (πβsuc π)) |
18 | 9, 17 | syl 17 |
. . . . . . . 8
β’ (π β Ο β ((π β Ο β¦ βͺ ran (πβπ))βsuc π) = βͺ ran (πβsuc π)) |
19 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
20 | 19 | rneqd 5938 |
. . . . . . . . . 10
β’ (π = π β ran (πβπ) = ran (πβπ)) |
21 | 20 | unieqd 4923 |
. . . . . . . . 9
β’ (π = π β βͺ ran
(πβπ) = βͺ ran (πβπ)) |
22 | | fvex 6905 |
. . . . . . . . . . 11
β’ (πβπ) β V |
23 | 22 | rnex 7903 |
. . . . . . . . . 10
β’ ran
(πβπ) β V |
24 | 23 | uniex 7731 |
. . . . . . . . 9
β’ βͺ ran (πβπ) β V |
25 | 21, 13, 24 | fvmpt 6999 |
. . . . . . . 8
β’ (π β Ο β ((π β Ο β¦ βͺ ran (πβπ))βπ) = βͺ ran (πβπ)) |
26 | 18, 25 | sseq12d 4016 |
. . . . . . 7
β’ (π β Ο β (((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β βͺ ran
(πβsuc π) β βͺ ran (πβπ))) |
27 | 26 | adantl 483 |
. . . . . 6
β’ ((π β§ π β Ο) β (((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β βͺ ran
(πβsuc π) β βͺ ran (πβπ))) |
28 | 8, 27 | mpbird 257 |
. . . . 5
β’ ((π β§ π β Ο) β ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
29 | 28 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
30 | 29 | adantr 482 |
. . 3
β’ ((π β§ πΊ β πΉ) β βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
31 | | fveq1 6891 |
. . . . . . 7
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (πβsuc π) = ((π β Ο β¦ βͺ ran (πβπ))βsuc π)) |
32 | | fveq1 6891 |
. . . . . . 7
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (πβπ) = ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
33 | 31, 32 | sseq12d 4016 |
. . . . . 6
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β ((πβsuc π) β (πβπ) β ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ))) |
34 | 33 | ralbidv 3178 |
. . . . 5
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (βπ β Ο (πβsuc π) β (πβπ) β βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ))) |
35 | | rneq 5936 |
. . . . . . 7
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β ran π = ran (π β Ο β¦ βͺ ran (πβπ))) |
36 | 35 | inteqd 4956 |
. . . . . 6
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β β© ran
π = β© ran (π β Ο β¦ βͺ ran (πβπ))) |
37 | 36, 35 | eleq12d 2828 |
. . . . 5
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (β© ran
π β ran π β β© ran (π β Ο β¦ βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ)))) |
38 | 34, 37 | imbi12d 345 |
. . . 4
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β ((βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π) β (βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β β© ran
(π β Ο β¦
βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ))))) |
39 | 1 | isfin3ds 10324 |
. . . . . 6
β’ (πΊ β πΉ β (πΊ β πΉ β βπ β (π« πΊ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π))) |
40 | 39 | ibi 267 |
. . . . 5
β’ (πΊ β πΉ β βπ β (π« πΊ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
41 | 40 | adantl 483 |
. . . 4
β’ ((π β§ πΊ β πΉ) β βπ β (π« πΊ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
42 | 1, 2, 3, 4, 5 | fin23lem34 10341 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β πΊ)) |
43 | 42 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π β Ο) β βͺ ran (πβπ) β πΊ) |
44 | 43 | adantlr 714 |
. . . . . . 7
β’ (((π β§ πΊ β πΉ) β§ π β Ο) β βͺ ran (πβπ) β πΊ) |
45 | | elpw2g 5345 |
. . . . . . . 8
β’ (πΊ β πΉ β (βͺ ran
(πβπ) β π« πΊ β βͺ ran
(πβπ) β πΊ)) |
46 | 45 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ πΊ β πΉ) β§ π β Ο) β (βͺ ran (πβπ) β π« πΊ β βͺ ran
(πβπ) β πΊ)) |
47 | 44, 46 | mpbird 257 |
. . . . . 6
β’ (((π β§ πΊ β πΉ) β§ π β Ο) β βͺ ran (πβπ) β π« πΊ) |
48 | 47 | fmpttd 7115 |
. . . . 5
β’ ((π β§ πΊ β πΉ) β (π β Ο β¦ βͺ ran (πβπ)):ΟβΆπ« πΊ) |
49 | | pwexg 5377 |
. . . . . 6
β’ (πΊ β πΉ β π« πΊ β V) |
50 | | vex 3479 |
. . . . . . . 8
β’ β β V |
51 | | f1f 6788 |
. . . . . . . 8
β’ (β:Οβ1-1βV β β:ΟβΆV) |
52 | | dmfex 7898 |
. . . . . . . 8
β’ ((β β V β§ β:ΟβΆV) β Ο
β V) |
53 | 50, 51, 52 | sylancr 588 |
. . . . . . 7
β’ (β:Οβ1-1βV β Ο β V) |
54 | 2, 53 | syl 17 |
. . . . . 6
β’ (π β Ο β
V) |
55 | | elmapg 8833 |
. . . . . 6
β’
((π« πΊ β
V β§ Ο β V) β ((π β Ο β¦ βͺ ran (πβπ)) β (π« πΊ βm Ο) β (π β Ο β¦ βͺ ran (πβπ)):ΟβΆπ« πΊ)) |
56 | 49, 54, 55 | syl2anr 598 |
. . . . 5
β’ ((π β§ πΊ β πΉ) β ((π β Ο β¦ βͺ ran (πβπ)) β (π« πΊ βm Ο) β (π β Ο β¦ βͺ ran (πβπ)):ΟβΆπ« πΊ)) |
57 | 48, 56 | mpbird 257 |
. . . 4
β’ ((π β§ πΊ β πΉ) β (π β Ο β¦ βͺ ran (πβπ)) β (π« πΊ βm
Ο)) |
58 | 38, 41, 57 | rspcdva 3614 |
. . 3
β’ ((π β§ πΊ β πΉ) β (βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β β© ran
(π β Ο β¦
βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ)))) |
59 | 30, 58 | mpd 15 |
. 2
β’ ((π β§ πΊ β πΉ) β β© ran
(π β Ο β¦
βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ))) |
60 | 6, 59 | mtand 815 |
1
β’ (π β Β¬ πΊ β πΉ) |