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 10346 |
. 2
β’ (π β Β¬ β© ran (π β Ο β¦ βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ))) |
7 | 1, 2, 3, 4, 5 | fin23lem35 10344 |
. . . . . . 7
β’ ((π β§ π β Ο) β βͺ ran (πβsuc π) β βͺ ran
(πβπ)) |
8 | 7 | pssssd 4096 |
. . . . . 6
β’ ((π β§ π β Ο) β βͺ ran (πβsuc π) β βͺ ran
(πβπ)) |
9 | | peano2 7883 |
. . . . . . . . 9
β’ (π β Ο β suc π β
Ο) |
10 | | fveq2 6890 |
. . . . . . . . . . . 12
β’ (π = suc π β (πβπ) = (πβsuc π)) |
11 | 10 | rneqd 5936 |
. . . . . . . . . . 11
β’ (π = suc π β ran (πβπ) = ran (πβsuc π)) |
12 | 11 | unieqd 4921 |
. . . . . . . . . 10
β’ (π = suc π β βͺ ran
(πβπ) = βͺ ran (πβsuc π)) |
13 | | eqid 2730 |
. . . . . . . . . 10
β’ (π β Ο β¦ βͺ ran (πβπ)) = (π β Ο β¦ βͺ ran (πβπ)) |
14 | | fvex 6903 |
. . . . . . . . . . . 12
β’ (πβsuc π) β V |
15 | 14 | rnex 7905 |
. . . . . . . . . . 11
β’ ran
(πβsuc π) β V |
16 | 15 | uniex 7733 |
. . . . . . . . . 10
β’ βͺ ran (πβsuc π) β V |
17 | 12, 13, 16 | fvmpt 6997 |
. . . . . . . . 9
β’ (suc
π β Ο β
((π β Ο β¦
βͺ ran (πβπ))βsuc π) = βͺ ran (πβsuc π)) |
18 | 9, 17 | syl 17 |
. . . . . . . 8
β’ (π β Ο β ((π β Ο β¦ βͺ ran (πβπ))βsuc π) = βͺ ran (πβsuc π)) |
19 | | fveq2 6890 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
20 | 19 | rneqd 5936 |
. . . . . . . . . 10
β’ (π = π β ran (πβπ) = ran (πβπ)) |
21 | 20 | unieqd 4921 |
. . . . . . . . 9
β’ (π = π β βͺ ran
(πβπ) = βͺ ran (πβπ)) |
22 | | fvex 6903 |
. . . . . . . . . . 11
β’ (πβπ) β V |
23 | 22 | rnex 7905 |
. . . . . . . . . 10
β’ ran
(πβπ) β V |
24 | 23 | uniex 7733 |
. . . . . . . . 9
β’ βͺ ran (πβπ) β V |
25 | 21, 13, 24 | fvmpt 6997 |
. . . . . . . 8
β’ (π β Ο β ((π β Ο β¦ βͺ ran (πβπ))βπ) = βͺ ran (πβπ)) |
26 | 18, 25 | sseq12d 4014 |
. . . . . . 7
β’ (π β Ο β (((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β βͺ ran
(πβsuc π) β βͺ ran (πβπ))) |
27 | 26 | adantl 480 |
. . . . . 6
β’ ((π β§ π β Ο) β (((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β βͺ ran
(πβsuc π) β βͺ ran (πβπ))) |
28 | 8, 27 | mpbird 256 |
. . . . 5
β’ ((π β§ π β Ο) β ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
29 | 28 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
30 | 29 | adantr 479 |
. . 3
β’ ((π β§ πΊ β πΉ) β βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
31 | | fveq1 6889 |
. . . . . . 7
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (πβsuc π) = ((π β Ο β¦ βͺ ran (πβπ))βsuc π)) |
32 | | fveq1 6889 |
. . . . . . 7
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (πβπ) = ((π β Ο β¦ βͺ ran (πβπ))βπ)) |
33 | 31, 32 | sseq12d 4014 |
. . . . . 6
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β ((πβsuc π) β (πβπ) β ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ))) |
34 | 33 | ralbidv 3175 |
. . . . 5
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (βπ β Ο (πβsuc π) β (πβπ) β βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ))) |
35 | | rneq 5934 |
. . . . . . 7
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β ran π = ran (π β Ο β¦ βͺ ran (πβπ))) |
36 | 35 | inteqd 4954 |
. . . . . 6
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β β© ran
π = β© ran (π β Ο β¦ βͺ ran (πβπ))) |
37 | 36, 35 | eleq12d 2825 |
. . . . 5
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β (β© ran
π β ran π β β© ran (π β Ο β¦ βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ)))) |
38 | 34, 37 | imbi12d 343 |
. . . 4
β’ (π = (π β Ο β¦ βͺ ran (πβπ)) β ((βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π) β (βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β β© ran
(π β Ο β¦
βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ))))) |
39 | 1 | isfin3ds 10326 |
. . . . . 6
β’ (πΊ β πΉ β (πΊ β πΉ β βπ β (π« πΊ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π))) |
40 | 39 | ibi 266 |
. . . . 5
β’ (πΊ β πΉ β βπ β (π« πΊ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
41 | 40 | adantl 480 |
. . . 4
β’ ((π β§ πΊ β πΉ) β βπ β (π« πΊ βm Ο)(βπ β Ο (πβsuc π) β (πβπ) β β© ran
π β ran π)) |
42 | 1, 2, 3, 4, 5 | fin23lem34 10343 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β πΊ)) |
43 | 42 | simprd 494 |
. . . . . . . 8
β’ ((π β§ π β Ο) β βͺ ran (πβπ) β πΊ) |
44 | 43 | adantlr 711 |
. . . . . . 7
β’ (((π β§ πΊ β πΉ) β§ π β Ο) β βͺ ran (πβπ) β πΊ) |
45 | | elpw2g 5343 |
. . . . . . . 8
β’ (πΊ β πΉ β (βͺ ran
(πβπ) β π« πΊ β βͺ ran
(πβπ) β πΊ)) |
46 | 45 | ad2antlr 723 |
. . . . . . 7
β’ (((π β§ πΊ β πΉ) β§ π β Ο) β (βͺ ran (πβπ) β π« πΊ β βͺ ran
(πβπ) β πΊ)) |
47 | 44, 46 | mpbird 256 |
. . . . . 6
β’ (((π β§ πΊ β πΉ) β§ π β Ο) β βͺ ran (πβπ) β π« πΊ) |
48 | 47 | fmpttd 7115 |
. . . . 5
β’ ((π β§ πΊ β πΉ) β (π β Ο β¦ βͺ ran (πβπ)):ΟβΆπ« πΊ) |
49 | | pwexg 5375 |
. . . . . 6
β’ (πΊ β πΉ β π« πΊ β V) |
50 | | vex 3476 |
. . . . . . . 8
β’ β β V |
51 | | f1f 6786 |
. . . . . . . 8
β’ (β:Οβ1-1βV β β:ΟβΆV) |
52 | | dmfex 7900 |
. . . . . . . 8
β’ ((β β V β§ β:ΟβΆV) β Ο
β V) |
53 | 50, 51, 52 | sylancr 585 |
. . . . . . 7
β’ (β:Οβ1-1βV β Ο β V) |
54 | 2, 53 | syl 17 |
. . . . . 6
β’ (π β Ο β
V) |
55 | | elmapg 8835 |
. . . . . 6
β’
((π« πΊ β
V β§ Ο β V) β ((π β Ο β¦ βͺ ran (πβπ)) β (π« πΊ βm Ο) β (π β Ο β¦ βͺ ran (πβπ)):ΟβΆπ« πΊ)) |
56 | 49, 54, 55 | syl2anr 595 |
. . . . 5
β’ ((π β§ πΊ β πΉ) β ((π β Ο β¦ βͺ ran (πβπ)) β (π« πΊ βm Ο) β (π β Ο β¦ βͺ ran (πβπ)):ΟβΆπ« πΊ)) |
57 | 48, 56 | mpbird 256 |
. . . 4
β’ ((π β§ πΊ β πΉ) β (π β Ο β¦ βͺ ran (πβπ)) β (π« πΊ βm
Ο)) |
58 | 38, 41, 57 | rspcdva 3612 |
. . 3
β’ ((π β§ πΊ β πΉ) β (βπ β Ο ((π β Ο β¦ βͺ ran (πβπ))βsuc π) β ((π β Ο β¦ βͺ ran (πβπ))βπ) β β© ran
(π β Ο β¦
βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ)))) |
59 | 30, 58 | mpd 15 |
. 2
β’ ((π β§ πΊ β πΉ) β β© ran
(π β Ο β¦
βͺ ran (πβπ)) β ran (π β Ο β¦ βͺ ran (πβπ))) |
60 | 6, 59 | mtand 812 |
1
β’ (π β Β¬ πΊ β πΉ) |