Step | Hyp | Ref
| Expression |
1 | | compss.a |
. . . . . . 7
β’ πΉ = (π₯ β π« π΄ β¦ (π΄ β π₯)) |
2 | 1 | isf34lem2 10333 |
. . . . . 6
β’ (π΄ β FinIII β
πΉ:π« π΄βΆπ« π΄) |
3 | 2 | adantr 481 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β πΉ:π« π΄βΆπ« π΄) |
4 | 3 | 3adant3 1132 |
. . . 4
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β πΉ:π« π΄βΆπ« π΄) |
5 | 4 | ffnd 6689 |
. . 3
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β πΉ Fn π« π΄) |
6 | | imassrn 6044 |
. . . 4
β’ (πΉ β ran πΊ) β ran πΉ |
7 | 3 | frnd 6696 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β ran πΉ β π« π΄) |
8 | 7 | 3adant3 1132 |
. . . 4
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β ran πΉ β π« π΄) |
9 | 6, 8 | sstrid 3973 |
. . 3
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β (πΉ β ran πΊ) β π« π΄) |
10 | | simp1 1136 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β π΄ β FinIII) |
11 | | fco 6712 |
. . . . . . 7
β’ ((πΉ:π« π΄βΆπ« π΄ β§ πΊ:ΟβΆπ« π΄) β (πΉ β πΊ):ΟβΆπ« π΄) |
12 | 2, 11 | sylan 580 |
. . . . . 6
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (πΉ β πΊ):ΟβΆπ« π΄) |
13 | 12 | 3adant3 1132 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β (πΉ β πΊ):ΟβΆπ« π΄) |
14 | | sscon 4118 |
. . . . . . . 8
β’ ((πΊβπ¦) β (πΊβsuc π¦) β (π΄ β (πΊβsuc π¦)) β (π΄ β (πΊβπ¦))) |
15 | | simpr 485 |
. . . . . . . . . . 11
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β πΊ:ΟβΆπ« π΄) |
16 | | peano2 7847 |
. . . . . . . . . . 11
β’ (π¦ β Ο β suc π¦ β
Ο) |
17 | | fvco3 6960 |
. . . . . . . . . . 11
β’ ((πΊ:ΟβΆπ« π΄ β§ suc π¦ β Ο) β ((πΉ β πΊ)βsuc π¦) = (πΉβ(πΊβsuc π¦))) |
18 | 15, 16, 17 | syl2an 596 |
. . . . . . . . . 10
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β ((πΉ β πΊ)βsuc π¦) = (πΉβ(πΊβsuc π¦))) |
19 | | simpll 765 |
. . . . . . . . . . 11
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β π΄ β FinIII) |
20 | | ffvelcdm 7052 |
. . . . . . . . . . . . 13
β’ ((πΊ:ΟβΆπ« π΄ β§ suc π¦ β Ο) β (πΊβsuc π¦) β π« π΄) |
21 | 15, 16, 20 | syl2an 596 |
. . . . . . . . . . . 12
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (πΊβsuc π¦) β π« π΄) |
22 | 21 | elpwid 4589 |
. . . . . . . . . . 11
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (πΊβsuc π¦) β π΄) |
23 | 1 | isf34lem1 10332 |
. . . . . . . . . . 11
β’ ((π΄ β FinIII β§
(πΊβsuc π¦) β π΄) β (πΉβ(πΊβsuc π¦)) = (π΄ β (πΊβsuc π¦))) |
24 | 19, 22, 23 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (πΉβ(πΊβsuc π¦)) = (π΄ β (πΊβsuc π¦))) |
25 | 18, 24 | eqtrd 2771 |
. . . . . . . . 9
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β ((πΉ β πΊ)βsuc π¦) = (π΄ β (πΊβsuc π¦))) |
26 | | fvco3 6960 |
. . . . . . . . . . 11
β’ ((πΊ:ΟβΆπ« π΄ β§ π¦ β Ο) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
27 | 26 | adantll 712 |
. . . . . . . . . 10
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
28 | | ffvelcdm 7052 |
. . . . . . . . . . . . 13
β’ ((πΊ:ΟβΆπ« π΄ β§ π¦ β Ο) β (πΊβπ¦) β π« π΄) |
29 | 28 | adantll 712 |
. . . . . . . . . . . 12
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (πΊβπ¦) β π« π΄) |
30 | 29 | elpwid 4589 |
. . . . . . . . . . 11
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (πΊβπ¦) β π΄) |
31 | 1 | isf34lem1 10332 |
. . . . . . . . . . 11
β’ ((π΄ β FinIII β§
(πΊβπ¦) β π΄) β (πΉβ(πΊβπ¦)) = (π΄ β (πΊβπ¦))) |
32 | 19, 30, 31 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (πΉβ(πΊβπ¦)) = (π΄ β (πΊβπ¦))) |
33 | 27, 32 | eqtrd 2771 |
. . . . . . . . 9
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β ((πΉ β πΊ)βπ¦) = (π΄ β (πΊβπ¦))) |
34 | 25, 33 | sseq12d 3995 |
. . . . . . . 8
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β (((πΉ β πΊ)βsuc π¦) β ((πΉ β πΊ)βπ¦) β (π΄ β (πΊβsuc π¦)) β (π΄ β (πΊβπ¦)))) |
35 | 14, 34 | imbitrrid 245 |
. . . . . . 7
β’ (((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β§ π¦ β Ο) β ((πΊβπ¦) β (πΊβsuc π¦) β ((πΉ β πΊ)βsuc π¦) β ((πΉ β πΊ)βπ¦))) |
36 | 35 | ralimdva 3166 |
. . . . . 6
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦) β βπ¦ β Ο ((πΉ β πΊ)βsuc π¦) β ((πΉ β πΊ)βπ¦))) |
37 | 36 | 3impia 1117 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β βπ¦ β Ο ((πΉ β πΊ)βsuc π¦) β ((πΉ β πΊ)βπ¦)) |
38 | | fin33i 10329 |
. . . . 5
β’ ((π΄ β FinIII β§
(πΉ β πΊ):ΟβΆπ« π΄ β§ βπ¦ β Ο ((πΉ β πΊ)βsuc π¦) β ((πΉ β πΊ)βπ¦)) β β© ran
(πΉ β πΊ) β ran (πΉ β πΊ)) |
39 | 10, 13, 37, 38 | syl3anc 1371 |
. . . 4
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β β© ran
(πΉ β πΊ) β ran (πΉ β πΊ)) |
40 | | rnco2 6225 |
. . . . 5
β’ ran
(πΉ β πΊ) = (πΉ β ran πΊ) |
41 | 40 | inteqi 4931 |
. . . 4
β’ β© ran (πΉ β πΊ) = β© (πΉ β ran πΊ) |
42 | 39, 41, 40 | 3eltr3g 2848 |
. . 3
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β β© (πΉ β ran πΊ) β (πΉ β ran πΊ)) |
43 | | fnfvima 7203 |
. . 3
β’ ((πΉ Fn π« π΄ β§ (πΉ β ran πΊ) β π« π΄ β§ β© (πΉ β ran πΊ) β (πΉ β ran πΊ)) β (πΉββ© (πΉ β ran πΊ)) β (πΉ β (πΉ β ran πΊ))) |
44 | 5, 9, 42, 43 | syl3anc 1371 |
. 2
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β (πΉββ© (πΉ β ran πΊ)) β (πΉ β (πΉ β ran πΊ))) |
45 | | simpl 483 |
. . . . . 6
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β π΄ β FinIII) |
46 | 6, 7 | sstrid 3973 |
. . . . . 6
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (πΉ β ran πΊ) β π« π΄) |
47 | | incom 4181 |
. . . . . . . . 9
β’ (dom
πΉ β© ran πΊ) = (ran πΊ β© dom πΉ) |
48 | | frn 6695 |
. . . . . . . . . . . 12
β’ (πΊ:ΟβΆπ« π΄ β ran πΊ β π« π΄) |
49 | 48 | adantl 482 |
. . . . . . . . . . 11
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β ran πΊ β π« π΄) |
50 | 3 | fdmd 6699 |
. . . . . . . . . . 11
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β dom πΉ = π« π΄) |
51 | 49, 50 | sseqtrrd 4003 |
. . . . . . . . . 10
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β ran πΊ β dom πΉ) |
52 | | df-ss 3945 |
. . . . . . . . . 10
β’ (ran
πΊ β dom πΉ β (ran πΊ β© dom πΉ) = ran πΊ) |
53 | 51, 52 | sylib 217 |
. . . . . . . . 9
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (ran πΊ β© dom πΉ) = ran πΊ) |
54 | 47, 53 | eqtrid 2783 |
. . . . . . . 8
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (dom πΉ β© ran πΊ) = ran πΊ) |
55 | | fdm 6697 |
. . . . . . . . . . 11
β’ (πΊ:ΟβΆπ« π΄ β dom πΊ = Ο) |
56 | 55 | adantl 482 |
. . . . . . . . . 10
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β dom πΊ = Ο) |
57 | | peano1 7845 |
. . . . . . . . . . 11
β’ β
β Ο |
58 | | ne0i 4314 |
. . . . . . . . . . 11
β’ (β
β Ο β Ο β β
) |
59 | 57, 58 | mp1i 13 |
. . . . . . . . . 10
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β Ο β
β
) |
60 | 56, 59 | eqnetrd 3007 |
. . . . . . . . 9
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β dom πΊ β β
) |
61 | | dm0rn0 5900 |
. . . . . . . . . 10
β’ (dom
πΊ = β
β ran
πΊ =
β
) |
62 | 61 | necon3bii 2992 |
. . . . . . . . 9
β’ (dom
πΊ β β
β ran
πΊ β
β
) |
63 | 60, 62 | sylib 217 |
. . . . . . . 8
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β ran πΊ β β
) |
64 | 54, 63 | eqnetrd 3007 |
. . . . . . 7
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (dom πΉ β© ran πΊ) β β
) |
65 | | imadisj 6052 |
. . . . . . . 8
β’ ((πΉ β ran πΊ) = β
β (dom πΉ β© ran πΊ) = β
) |
66 | 65 | necon3bii 2992 |
. . . . . . 7
β’ ((πΉ β ran πΊ) β β
β (dom πΉ β© ran πΊ) β β
) |
67 | 64, 66 | sylibr 233 |
. . . . . 6
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (πΉ β ran πΊ) β β
) |
68 | 1 | isf34lem5 10338 |
. . . . . 6
β’ ((π΄ β FinIII β§
((πΉ β ran πΊ) β π« π΄ β§ (πΉ β ran πΊ) β β
)) β (πΉββ© (πΉ β ran πΊ)) = βͺ (πΉ β (πΉ β ran πΊ))) |
69 | 45, 46, 67, 68 | syl12anc 835 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (πΉββ© (πΉ
β ran πΊ)) = βͺ (πΉ
β (πΉ β ran
πΊ))) |
70 | 1 | isf34lem3 10335 |
. . . . . . 7
β’ ((π΄ β FinIII β§
ran πΊ β π«
π΄) β (πΉ β (πΉ β ran πΊ)) = ran πΊ) |
71 | 45, 49, 70 | syl2anc 584 |
. . . . . 6
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (πΉ β (πΉ β ran πΊ)) = ran πΊ) |
72 | 71 | unieqd 4899 |
. . . . 5
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β βͺ (πΉ
β (πΉ β ran
πΊ)) = βͺ ran πΊ) |
73 | 69, 72 | eqtrd 2771 |
. . . 4
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β (πΉββ© (πΉ
β ran πΊ)) = βͺ ran πΊ) |
74 | 73, 71 | eleq12d 2826 |
. . 3
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄) β ((πΉββ© (πΉ
β ran πΊ)) β
(πΉ β (πΉ β ran πΊ)) β βͺ ran
πΊ β ran πΊ)) |
75 | 74 | 3adant3 1132 |
. 2
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β ((πΉββ© (πΉ β ran πΊ)) β (πΉ β (πΉ β ran πΊ)) β βͺ ran
πΊ β ran πΊ)) |
76 | 44, 75 | mpbid 231 |
1
β’ ((π΄ β FinIII β§
πΊ:ΟβΆπ«
π΄ β§ βπ¦ β Ο (πΊβπ¦) β (πΊβsuc π¦)) β βͺ ran
πΊ β ran πΊ) |