Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . . 4
β’ βΌ = (
~FG βπΌ) |
3 | | efgval2.m |
. . . 4
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
4 | | efgval2.t |
. . . 4
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
5 | | efgred.d |
. . . 4
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
6 | | efgred.s |
. . . 4
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsf 19518 |
. . 3
β’ π:{π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))}βΆπ |
8 | 7 | fdmi 6685 |
. . . 4
β’ dom π = {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} |
9 | 8 | feq2i 6665 |
. . 3
β’ (π:dom πβΆπ β π:{π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))}βΆπ) |
10 | 7, 9 | mpbir 230 |
. 2
β’ π:dom πβΆπ |
11 | | frn 6680 |
. . . 4
β’ (π:dom πβΆπ β ran π β π) |
12 | 10, 11 | ax-mp 5 |
. . 3
β’ ran π β π |
13 | | fviss 6923 |
. . . . . . . . 9
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
14 | 1, 13 | eqsstri 3983 |
. . . . . . . 8
β’ π β Word (πΌ Γ 2o) |
15 | 14 | sseli 3945 |
. . . . . . 7
β’ (π β π β π β Word (πΌ Γ 2o)) |
16 | | lencl 14428 |
. . . . . . 7
β’ (π β Word (πΌ Γ 2o) β
(β―βπ) β
β0) |
17 | 15, 16 | syl 17 |
. . . . . 6
β’ (π β π β (β―βπ) β
β0) |
18 | | peano2nn0 12460 |
. . . . . 6
β’
((β―βπ)
β β0 β ((β―βπ) + 1) β
β0) |
19 | 14 | sseli 3945 |
. . . . . . . . . . . 12
β’ (π β π β π β Word (πΌ Γ 2o)) |
20 | | lencl 14428 |
. . . . . . . . . . . 12
β’ (π β Word (πΌ Γ 2o) β
(β―βπ) β
β0) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β (β―βπ) β
β0) |
22 | | nn0nlt0 12446 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β Β¬ (β―βπ) < 0) |
23 | | breq2 5114 |
. . . . . . . . . . . . 13
β’ (π = 0 β
((β―βπ) <
π β
(β―βπ) <
0)) |
24 | 23 | notbid 318 |
. . . . . . . . . . . 12
β’ (π = 0 β (Β¬
(β―βπ) <
π β Β¬
(β―βπ) <
0)) |
25 | 22, 24 | syl5ibr 246 |
. . . . . . . . . . 11
β’ (π = 0 β
((β―βπ) β
β0 β Β¬ (β―βπ) < π)) |
26 | 21, 25 | syl5 34 |
. . . . . . . . . 10
β’ (π = 0 β (π β π β Β¬ (β―βπ) < π)) |
27 | 26 | ralrimiv 3143 |
. . . . . . . . 9
β’ (π = 0 β βπ β π Β¬ (β―βπ) < π) |
28 | | rabeq0 4349 |
. . . . . . . . 9
β’ ({π β π β£ (β―βπ) < π} = β
β βπ β π Β¬ (β―βπ) < π) |
29 | 27, 28 | sylibr 233 |
. . . . . . . 8
β’ (π = 0 β {π β π β£ (β―βπ) < π} = β
) |
30 | 29 | sseq1d 3980 |
. . . . . . 7
β’ (π = 0 β ({π β π β£ (β―βπ) < π} β ran π β β
β ran π)) |
31 | | breq2 5114 |
. . . . . . . . 9
β’ (π = π β ((β―βπ) < π β (β―βπ) < π)) |
32 | 31 | rabbidv 3418 |
. . . . . . . 8
β’ (π = π β {π β π β£ (β―βπ) < π} = {π β π β£ (β―βπ) < π}) |
33 | 32 | sseq1d 3980 |
. . . . . . 7
β’ (π = π β ({π β π β£ (β―βπ) < π} β ran π β {π β π β£ (β―βπ) < π} β ran π)) |
34 | | breq2 5114 |
. . . . . . . . 9
β’ (π = (π + 1) β ((β―βπ) < π β (β―βπ) < (π + 1))) |
35 | 34 | rabbidv 3418 |
. . . . . . . 8
β’ (π = (π + 1) β {π β π β£ (β―βπ) < π} = {π β π β£ (β―βπ) < (π + 1)}) |
36 | 35 | sseq1d 3980 |
. . . . . . 7
β’ (π = (π + 1) β ({π β π β£ (β―βπ) < π} β ran π β {π β π β£ (β―βπ) < (π + 1)} β ran π)) |
37 | | breq2 5114 |
. . . . . . . . 9
β’ (π = ((β―βπ) + 1) β
((β―βπ) <
π β
(β―βπ) <
((β―βπ) +
1))) |
38 | 37 | rabbidv 3418 |
. . . . . . . 8
β’ (π = ((β―βπ) + 1) β {π β π β£ (β―βπ) < π} = {π β π β£ (β―βπ) < ((β―βπ) + 1)}) |
39 | 38 | sseq1d 3980 |
. . . . . . 7
β’ (π = ((β―βπ) + 1) β ({π β π β£ (β―βπ) < π} β ran π β {π β π β£ (β―βπ) < ((β―βπ) + 1)} β ran π)) |
40 | | 0ss 4361 |
. . . . . . 7
β’ β
β ran π |
41 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β {π β π β£ (β―βπ) < π} β ran π) |
42 | | fveqeq2 6856 |
. . . . . . . . . . . 12
β’ (π = π β ((β―βπ) = π β (β―βπ) = π)) |
43 | 42 | cbvrabv 3420 |
. . . . . . . . . . 11
β’ {π β π β£ (β―βπ) = π} = {π β π β£ (β―βπ) = π} |
44 | | eliun 4963 |
. . . . . . . . . . . . . . 15
β’ (π β βͺ π₯ β π ran (πβπ₯) β βπ₯ β π π β ran (πβπ₯)) |
45 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
46 | 45 | rneqd 5898 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ran (πβπ₯) = ran (πβπ)) |
47 | 46 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π β ran (πβπ₯) β π β ran (πβπ))) |
48 | 47 | cbvrexvw 3229 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
π π β ran (πβπ₯) β βπ β π π β ran (πβπ)) |
49 | 44, 48 | bitri 275 |
. . . . . . . . . . . . . 14
β’ (π β βͺ π₯ β π ran (πβπ₯) β βπ β π π β ran (πβπ)) |
50 | | simpl1r 1226 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β {π β π β£ (β―βπ) < π} β ran π) |
51 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (β―βπ) = (β―βπ)) |
52 | 51 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((β―βπ) < π β (β―βπ) < π)) |
53 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β π β π) |
54 | 14, 53 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β π β Word (πΌ Γ 2o)) |
55 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Word (πΌ Γ 2o) β
(β―βπ) β
β0) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β (β―βπ) β
β0) |
57 | 56 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β (β―βπ) β β) |
58 | | 2rp 12927 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
β+ |
59 | | ltaddrp 12959 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β β β§ 2 β β+) β (β―βπ) < ((β―βπ) + 2)) |
60 | 57, 58, 59 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β (β―βπ) < ((β―βπ) + 2)) |
61 | 1, 2, 3, 4 | efgtlen 19515 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π β§ π β ran (πβπ)) β (β―βπ) = ((β―βπ) + 2)) |
62 | 61 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β (β―βπ) = ((β―βπ) + 2)) |
63 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β (β―βπ) = π) |
64 | 62, 63 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β ((β―βπ) + 2) = π) |
65 | 60, 64 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β (β―βπ) < π) |
66 | 52, 53, 65 | elrabd 3652 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β π β {π β π β£ (β―βπ) < π}) |
67 | 50, 66 | sseldd 3950 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β π β ran π) |
68 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:dom πβΆπ β π Fn dom π) |
69 | 10, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ π Fn dom π |
70 | | fvelrnb 6908 |
. . . . . . . . . . . . . . . . . 18
β’ (π Fn dom π β (π β ran π β βπ β dom π(πβπ) = π)) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (π β ran π β βπ β dom π(πβπ) = π) |
72 | 67, 71 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β βπ β dom π(πβπ) = π) |
73 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β π β dom π) |
74 | 1, 2, 3, 4, 5, 6 | efgsdm 19519 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β dom π β (π β (Word π β {β
}) β§ (πβ0) β π· β§ βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))) |
75 | 74 | simp1bi 1146 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom π β π β (Word π β {β
})) |
76 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Word π β {β
}) β π β Word π) |
77 | 73, 75, 76 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β π β Word π) |
78 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β π β π) |
79 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β π β ran (πβπ)) |
80 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β (πβπ) = π) |
81 | 80 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β (πβ(πβπ)) = (πβπ)) |
82 | 81 | rneqd 5898 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β ran (πβ(πβπ)) = ran (πβπ)) |
83 | 79, 82 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β π β ran (πβ(πβπ))) |
84 | 1, 2, 3, 4, 5, 6 | efgsp1 19526 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom π β§ π β ran (πβ(πβπ))) β (π ++ β¨βπββ©) β dom π) |
85 | 73, 83, 84 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β (π ++ β¨βπββ©) β dom π) |
86 | 1, 2, 3, 4, 5, 6 | efgsval2 19522 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ π β π β§ (π ++ β¨βπββ©) β dom π) β (πβ(π ++ β¨βπββ©)) = π) |
87 | 77, 78, 85, 86 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β (πβ(π ++ β¨βπββ©)) = π) |
88 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π Fn dom π β§ (π ++ β¨βπββ©) β dom π) β (πβ(π ++ β¨βπββ©)) β ran π) |
89 | 69, 85, 88 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β (πβ(π ++ β¨βπββ©)) β ran π) |
90 | 87, 89 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ ((π β π β§ π β ran (πβπ)) β§ (π β dom π β§ (πβπ) = π))) β π β ran π) |
91 | 90 | anassrs 469 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β0 β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β§ (π β dom π β§ (πβπ) = π)) β π β ran π) |
92 | 72, 91 | rexlimddv 3159 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β§ (π β π β§ π β ran (πβπ))) β π β ran π) |
93 | 92 | rexlimdvaa 3154 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β (βπ β π π β ran (πβπ) β π β ran π)) |
94 | 49, 93 | biimtrid 241 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β (π β βͺ
π₯ β π ran (πβπ₯) β π β ran π)) |
95 | | eldif 3925 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β βͺ
π₯ β π ran (πβπ₯)) β (π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯))) |
96 | 5 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π· β π β (π β βͺ
π₯ β π ran (πβπ₯))) |
97 | 1, 2, 3, 4, 5, 6 | efgs1 19524 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π· β β¨βπββ© β dom π) |
98 | 96, 97 | sylbir 234 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β βͺ
π₯ β π ran (πβπ₯)) β β¨βπββ© β dom π) |
99 | 95, 98 | sylbir 234 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β β¨βπββ© β dom π) |
100 | 1, 2, 3, 4, 5, 6 | efgsval 19520 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨βπββ© β dom π β (πββ¨βπββ©) = (β¨βπββ©β((β―ββ¨βπββ©) β
1))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β (πββ¨βπββ©) = (β¨βπββ©β((β―ββ¨βπββ©) β
1))) |
102 | | s1len 14501 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β―ββ¨βπββ©) = 1 |
103 | 102 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―ββ¨βπββ©) β 1) = (1 β
1) |
104 | | 1m1e0 12232 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1
β 1) = 0 |
105 | 103, 104 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―ββ¨βπββ©) β 1) =
0 |
106 | 105 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨βπββ©β((β―ββ¨βπββ©) β 1)) =
(β¨βπββ©β0) |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β (β¨βπββ©β((β―ββ¨βπββ©) β 1)) =
(β¨βπββ©β0)) |
108 | | s1fv 14505 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (β¨βπββ©β0) = π) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β (β¨βπββ©β0) = π) |
110 | 101, 107,
109 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β (πββ¨βπββ©) = π) |
111 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . . 17
β’ ((π Fn dom π β§ β¨βπββ© β dom π) β (πββ¨βπββ©) β ran π) |
112 | 69, 99, 111 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β (πββ¨βπββ©) β ran π) |
113 | 110, 112 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ Β¬ π β βͺ
π₯ β π ran (πβπ₯)) β π β ran π) |
114 | 113 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β π β (Β¬ π β βͺ
π₯ β π ran (πβπ₯) β π β ran π)) |
115 | 114 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β (Β¬ π β βͺ
π₯ β π ran (πβπ₯) β π β ran π)) |
116 | 94, 115 | pm2.61d 179 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β§ π β π β§ (β―βπ) = π) β π β ran π) |
117 | 116 | rabssdv 4037 |
. . . . . . . . . . 11
β’ ((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β {π β π β£ (β―βπ) = π} β ran π) |
118 | 43, 117 | eqsstrid 3997 |
. . . . . . . . . 10
β’ ((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β {π β π β£ (β―βπ) = π} β ran π) |
119 | 41, 118 | unssd 4151 |
. . . . . . . . 9
β’ ((π β β0
β§ {π β π β£ (β―βπ) < π} β ran π) β ({π β π β£ (β―βπ) < π} βͺ {π β π β£ (β―βπ) = π}) β ran π) |
120 | 119 | ex 414 |
. . . . . . . 8
β’ (π β β0
β ({π β π β£ (β―βπ) < π} β ran π β ({π β π β£ (β―βπ) < π} βͺ {π β π β£ (β―βπ) = π}) β ran π)) |
121 | | id 22 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β0) |
122 | | nn0leltp1 12569 |
. . . . . . . . . . . . 13
β’
(((β―βπ)
β β0 β§ π β β0) β
((β―βπ) β€
π β
(β―βπ) <
(π + 1))) |
123 | 21, 121, 122 | syl2anr 598 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β π) β ((β―βπ) β€ π β (β―βπ) < (π + 1))) |
124 | 21 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ (π β π β (β―βπ) β β) |
125 | | nn0re 12429 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
126 | | leloe 11248 |
. . . . . . . . . . . . 13
β’
(((β―βπ)
β β β§ π
β β) β ((β―βπ) β€ π β ((β―βπ) < π β¨ (β―βπ) = π))) |
127 | 124, 125,
126 | syl2anr 598 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β π) β ((β―βπ) β€ π β ((β―βπ) < π β¨ (β―βπ) = π))) |
128 | 123, 127 | bitr3d 281 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β π) β ((β―βπ) < (π + 1) β ((β―βπ) < π β¨ (β―βπ) = π))) |
129 | 128 | rabbidva 3417 |
. . . . . . . . . 10
β’ (π β β0
β {π β π β£ (β―βπ) < (π + 1)} = {π β π β£ ((β―βπ) < π β¨ (β―βπ) = π)}) |
130 | | unrab 4270 |
. . . . . . . . . 10
β’ ({π β π β£ (β―βπ) < π} βͺ {π β π β£ (β―βπ) = π}) = {π β π β£ ((β―βπ) < π β¨ (β―βπ) = π)} |
131 | 129, 130 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π β β0
β {π β π β£ (β―βπ) < (π + 1)} = ({π β π β£ (β―βπ) < π} βͺ {π β π β£ (β―βπ) = π})) |
132 | 131 | sseq1d 3980 |
. . . . . . . 8
β’ (π β β0
β ({π β π β£ (β―βπ) < (π + 1)} β ran π β ({π β π β£ (β―βπ) < π} βͺ {π β π β£ (β―βπ) = π}) β ran π)) |
133 | 120, 132 | sylibrd 259 |
. . . . . . 7
β’ (π β β0
β ({π β π β£ (β―βπ) < π} β ran π β {π β π β£ (β―βπ) < (π + 1)} β ran π)) |
134 | 30, 33, 36, 39, 40, 133 | nn0ind 12605 |
. . . . . 6
β’
(((β―βπ)
+ 1) β β0 β {π β π β£ (β―βπ) < ((β―βπ) + 1)} β ran π) |
135 | 17, 18, 134 | 3syl 18 |
. . . . 5
β’ (π β π β {π β π β£ (β―βπ) < ((β―βπ) + 1)} β ran π) |
136 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (β―βπ) = (β―βπ)) |
137 | 136 | breq1d 5120 |
. . . . . 6
β’ (π = π β ((β―βπ) < ((β―βπ) + 1) β (β―βπ) < ((β―βπ) + 1))) |
138 | | id 22 |
. . . . . 6
β’ (π β π β π β π) |
139 | 17 | nn0red 12481 |
. . . . . . 7
β’ (π β π β (β―βπ) β β) |
140 | 139 | ltp1d 12092 |
. . . . . 6
β’ (π β π β (β―βπ) < ((β―βπ) + 1)) |
141 | 137, 138,
140 | elrabd 3652 |
. . . . 5
β’ (π β π β π β {π β π β£ (β―βπ) < ((β―βπ) + 1)}) |
142 | 135, 141 | sseldd 3950 |
. . . 4
β’ (π β π β π β ran π) |
143 | 142 | ssriv 3953 |
. . 3
β’ π β ran π |
144 | 12, 143 | eqssi 3965 |
. 2
β’ ran π = π |
145 | | dffo2 6765 |
. 2
β’ (π:dom πβontoβπ β (π:dom πβΆπ β§ ran π = π)) |
146 | 10, 144, 145 | mpbir2an 710 |
1
β’ π:dom πβontoβπ |