Step | Hyp | Ref
| Expression |
1 | | ennnfonelemkh.p |
. 2
β’ (π β π β
β0) |
2 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = 0 β (π»βπ€) = (π»β0)) |
3 | 2 | dmeqd 4829 |
. . . . . 6
β’ (π€ = 0 β dom (π»βπ€) = dom (π»β0)) |
4 | | fveq2 5515 |
. . . . . 6
β’ (π€ = 0 β (β‘πβπ€) = (β‘πβ0)) |
5 | 3, 4 | sseq12d 3186 |
. . . . 5
β’ (π€ = 0 β (dom (π»βπ€) β (β‘πβπ€) β dom (π»β0) β (β‘πβ0))) |
6 | 5 | imbi2d 230 |
. . . 4
β’ (π€ = 0 β ((π β dom (π»βπ€) β (β‘πβπ€)) β (π β dom (π»β0) β (β‘πβ0)))) |
7 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = π β (π»βπ€) = (π»βπ)) |
8 | 7 | dmeqd 4829 |
. . . . . 6
β’ (π€ = π β dom (π»βπ€) = dom (π»βπ)) |
9 | | fveq2 5515 |
. . . . . 6
β’ (π€ = π β (β‘πβπ€) = (β‘πβπ)) |
10 | 8, 9 | sseq12d 3186 |
. . . . 5
β’ (π€ = π β (dom (π»βπ€) β (β‘πβπ€) β dom (π»βπ) β (β‘πβπ))) |
11 | 10 | imbi2d 230 |
. . . 4
β’ (π€ = π β ((π β dom (π»βπ€) β (β‘πβπ€)) β (π β dom (π»βπ) β (β‘πβπ)))) |
12 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = (π + 1) β (π»βπ€) = (π»β(π + 1))) |
13 | 12 | dmeqd 4829 |
. . . . . 6
β’ (π€ = (π + 1) β dom (π»βπ€) = dom (π»β(π + 1))) |
14 | | fveq2 5515 |
. . . . . 6
β’ (π€ = (π + 1) β (β‘πβπ€) = (β‘πβ(π + 1))) |
15 | 13, 14 | sseq12d 3186 |
. . . . 5
β’ (π€ = (π + 1) β (dom (π»βπ€) β (β‘πβπ€) β dom (π»β(π + 1)) β (β‘πβ(π + 1)))) |
16 | 15 | imbi2d 230 |
. . . 4
β’ (π€ = (π + 1) β ((π β dom (π»βπ€) β (β‘πβπ€)) β (π β dom (π»β(π + 1)) β (β‘πβ(π + 1))))) |
17 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = π β (π»βπ€) = (π»βπ)) |
18 | 17 | dmeqd 4829 |
. . . . . 6
β’ (π€ = π β dom (π»βπ€) = dom (π»βπ)) |
19 | | fveq2 5515 |
. . . . . 6
β’ (π€ = π β (β‘πβπ€) = (β‘πβπ)) |
20 | 18, 19 | sseq12d 3186 |
. . . . 5
β’ (π€ = π β (dom (π»βπ€) β (β‘πβπ€) β dom (π»βπ) β (β‘πβπ))) |
21 | 20 | imbi2d 230 |
. . . 4
β’ (π€ = π β ((π β dom (π»βπ€) β (β‘πβπ€)) β (π β dom (π»βπ) β (β‘πβπ)))) |
22 | | ennnfonelemh.dceq |
. . . . . . . . 9
β’ (π β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
23 | | ennnfonelemh.f |
. . . . . . . . 9
β’ (π β πΉ:Οβontoβπ΄) |
24 | | ennnfonelemh.ne |
. . . . . . . . 9
β’ (π β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
25 | | ennnfonelemh.g |
. . . . . . . . 9
β’ πΊ = (π₯ β (π΄ βpm Ο), π¦ β Ο β¦
if((πΉβπ¦) β (πΉ β π¦), π₯, (π₯ βͺ {β¨dom π₯, (πΉβπ¦)β©}))) |
26 | | ennnfonelemh.n |
. . . . . . . . 9
β’ π = frec((π₯ β β€ β¦ (π₯ + 1)), 0) |
27 | | ennnfonelemh.j |
. . . . . . . . 9
β’ π½ = (π₯ β β0 β¦ if(π₯ = 0, β
, (β‘πβ(π₯ β 1)))) |
28 | | ennnfonelemh.h |
. . . . . . . . 9
β’ π» = seq0(πΊ, π½) |
29 | 22, 23, 24, 25, 26, 27, 28 | ennnfonelem0 12405 |
. . . . . . . 8
β’ (π β (π»β0) = β
) |
30 | 29 | dmeqd 4829 |
. . . . . . 7
β’ (π β dom (π»β0) = dom β
) |
31 | | dm0 4841 |
. . . . . . 7
β’ dom
β
= β
|
32 | 30, 31 | eqtrdi 2226 |
. . . . . 6
β’ (π β dom (π»β0) = β
) |
33 | | 0ss 3461 |
. . . . . 6
β’ β
β (β‘πβ0) |
34 | 32, 33 | eqsstrdi 3207 |
. . . . 5
β’ (π β dom (π»β0) β (β‘πβ0)) |
35 | 34 | a1i 9 |
. . . 4
β’ (0 β
β€ β (π β dom
(π»β0) β (β‘πβ0))) |
36 | 26 | frechashgf1o 10427 |
. . . . . . . . . . . . . 14
β’ π:Οβ1-1-ontoββ0 |
37 | | f1of 5461 |
. . . . . . . . . . . . . 14
β’ (π:Οβ1-1-ontoββ0 β π:ΟβΆβ0) |
38 | 36, 37 | mp1i 10 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β π:ΟβΆβ0) |
39 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
40 | 23 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β πΉ:Οβontoβπ΄) |
41 | 24 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
42 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β π β
(β€β₯β0)) |
43 | | nn0uz 9561 |
. . . . . . . . . . . . . . . . 17
β’
β0 = (β€β₯β0) |
44 | 42, 43 | eleqtrrdi 2271 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β π β β0) |
45 | | peano2nn0 9215 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β0) |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (π + 1) β
β0) |
47 | 39, 40, 41, 25, 26, 27, 28, 46 | ennnfonelemom 12408 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β dom (π»β(π + 1)) β Ο) |
48 | 47 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) β Ο) |
49 | 38, 48 | ffvelcdmd 5652 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β
β0) |
50 | 49 | nn0red 9229 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β β) |
51 | 44 | nn0red 9229 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β π β β) |
52 | 51 | adantr 276 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β π β β) |
53 | | peano2re 8092 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β) |
54 | 52, 53 | syl 14 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (π + 1) β β) |
55 | 39, 40, 41, 25, 26, 27, 28, 44 | ennnfonelemp1 12406 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (π»β(π + 1)) = if((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)), (π»βπ), ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©}))) |
56 | 55 | adantr 276 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (π»β(π + 1)) = if((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)), (π»βπ), ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©}))) |
57 | | simpr 110 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) |
58 | 57 | iftrued 3541 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β if((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)), (π»βπ), ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©})) = (π»βπ)) |
59 | 56, 58 | eqtrd 2210 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (π»β(π + 1)) = (π»βπ)) |
60 | 59 | dmeqd 4829 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) = dom (π»βπ)) |
61 | 60 | fveq2d 5519 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) = (πβdom (π»βπ))) |
62 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β dom (π»βπ) β (β‘πβπ)) |
63 | | 0zd 9264 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β 0 β β€) |
64 | 39, 40, 41, 25, 26, 27, 28, 44 | ennnfonelemom 12408 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β dom (π»βπ) β Ο) |
65 | | f1ocnv 5474 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:Οβ1-1-ontoββ0 β β‘π:β0β1-1-ontoβΟ) |
66 | 36, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ β‘π:β0β1-1-ontoβΟ |
67 | | f1of 5461 |
. . . . . . . . . . . . . . . . . . 19
β’ (β‘π:β0β1-1-ontoβΟ β β‘π:β0βΆΟ) |
68 | 66, 67 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β β‘π:β0βΆΟ) |
69 | | id 19 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β π β
β0) |
70 | 68, 69 | ffvelcdmd 5652 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (β‘πβπ) β Ο) |
71 | 44, 70 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (β‘πβπ) β Ο) |
72 | 63, 26, 64, 71 | frec2uzled 10428 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (dom (π»βπ) β (β‘πβπ) β (πβdom (π»βπ)) β€ (πβ(β‘πβπ)))) |
73 | 62, 72 | mpbid 147 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (πβdom (π»βπ)) β€ (πβ(β‘πβπ))) |
74 | | f1ocnvfv2 5778 |
. . . . . . . . . . . . . . 15
β’ ((π:Οβ1-1-ontoββ0 β§ π β β0) β (πβ(β‘πβπ)) = π) |
75 | 36, 44, 74 | sylancr 414 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (πβ(β‘πβπ)) = π) |
76 | 73, 75 | breqtrd 4029 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (πβdom (π»βπ)) β€ π) |
77 | 76 | adantr 276 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»βπ)) β€ π) |
78 | 61, 77 | eqbrtrd 4025 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β€ π) |
79 | 52 | lep1d 8887 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β π β€ (π + 1)) |
80 | 50, 52, 54, 78, 79 | letrd 8080 |
. . . . . . . . . 10
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β€ (π + 1)) |
81 | | f1ocnvfv2 5778 |
. . . . . . . . . . . 12
β’ ((π:Οβ1-1-ontoββ0 β§ (π + 1) β β0) β
(πβ(β‘πβ(π + 1))) = (π + 1)) |
82 | 36, 46, 81 | sylancr 414 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (πβ(β‘πβ(π + 1))) = (π + 1)) |
83 | 82 | adantr 276 |
. . . . . . . . . 10
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβ(β‘πβ(π + 1))) = (π + 1)) |
84 | 80, 83 | breqtrrd 4031 |
. . . . . . . . 9
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β€ (πβ(β‘πβ(π + 1)))) |
85 | 66, 67 | mp1i 10 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β β‘π:β0βΆΟ) |
86 | 85, 46 | ffvelcdmd 5652 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (β‘πβ(π + 1)) β Ο) |
87 | 63, 26, 47, 86 | frec2uzled 10428 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (dom (π»β(π + 1)) β (β‘πβ(π + 1)) β (πβdom (π»β(π + 1))) β€ (πβ(β‘πβ(π + 1))))) |
88 | 87 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (dom (π»β(π + 1)) β (β‘πβ(π + 1)) β (πβdom (π»β(π + 1))) β€ (πβ(β‘πβ(π + 1))))) |
89 | 84, 88 | mpbird 167 |
. . . . . . . 8
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) β (β‘πβ(π + 1))) |
90 | 55 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (π»β(π + 1)) = if((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)), (π»βπ), ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©}))) |
91 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) |
92 | 91 | iffalsed 3544 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β if((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)), (π»βπ), ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©})) = ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©})) |
93 | 90, 92 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (π»β(π + 1)) = ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©})) |
94 | 93 | dmeqd 4829 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) = dom ((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©})) |
95 | | dmun 4834 |
. . . . . . . . . . . . . . . 16
β’ dom
((π»βπ) βͺ {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©}) = (dom (π»βπ) βͺ dom {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©}) |
96 | 94, 95 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) = (dom (π»βπ) βͺ dom {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©})) |
97 | | fof 5438 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ:Οβontoβπ΄ β πΉ:ΟβΆπ΄) |
98 | 40, 97 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β πΉ:ΟβΆπ΄) |
99 | 98, 71 | ffvelcdmd 5652 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β (πΉβ(β‘πβπ)) β π΄) |
100 | 99 | adantr 276 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πΉβ(β‘πβπ)) β π΄) |
101 | | dmsnopg 5100 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβ(β‘πβπ)) β π΄ β dom {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©} = {dom (π»βπ)}) |
102 | 100, 101 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©} = {dom (π»βπ)}) |
103 | 102 | uneq2d 3289 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (dom (π»βπ) βͺ dom {β¨dom (π»βπ), (πΉβ(β‘πβπ))β©}) = (dom (π»βπ) βͺ {dom (π»βπ)})) |
104 | 96, 103 | eqtrd 2210 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) = (dom (π»βπ) βͺ {dom (π»βπ)})) |
105 | | df-suc 4371 |
. . . . . . . . . . . . . 14
β’ suc dom
(π»βπ) = (dom (π»βπ) βͺ {dom (π»βπ)}) |
106 | 104, 105 | eqtr4di 2228 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) = suc dom (π»βπ)) |
107 | | simplr 528 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»βπ) β (β‘πβπ)) |
108 | 71 | adantr 276 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (β‘πβπ) β Ο) |
109 | | nnsucsssuc 6492 |
. . . . . . . . . . . . . . 15
β’ ((dom
(π»βπ) β Ο β§ (β‘πβπ) β Ο) β (dom (π»βπ) β (β‘πβπ) β suc dom (π»βπ) β suc (β‘πβπ))) |
110 | 64, 108, 109 | syl2an2r 595 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (dom (π»βπ) β (β‘πβπ) β suc dom (π»βπ) β suc (β‘πβπ))) |
111 | 107, 110 | mpbid 147 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β suc dom (π»βπ) β suc (β‘πβπ)) |
112 | 106, 111 | eqsstrd 3191 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) β suc (β‘πβπ)) |
113 | | 0zd 9264 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β 0 β β€) |
114 | 47 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) β Ο) |
115 | | peano2 4594 |
. . . . . . . . . . . . . 14
β’ ((β‘πβπ) β Ο β suc (β‘πβπ) β Ο) |
116 | 108, 115 | syl 14 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β suc (β‘πβπ) β Ο) |
117 | 113, 26, 114, 116 | frec2uzled 10428 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (dom (π»β(π + 1)) β suc (β‘πβπ) β (πβdom (π»β(π + 1))) β€ (πβsuc (β‘πβπ)))) |
118 | 112, 117 | mpbid 147 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β€ (πβsuc (β‘πβπ))) |
119 | 113, 26, 108 | frec2uzsucd 10400 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβsuc (β‘πβπ)) = ((πβ(β‘πβπ)) + 1)) |
120 | 75 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβ(β‘πβπ)) = π) |
121 | 120 | oveq1d 5889 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β ((πβ(β‘πβπ)) + 1) = (π + 1)) |
122 | 119, 121 | eqtrd 2210 |
. . . . . . . . . . 11
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβsuc (β‘πβπ)) = (π + 1)) |
123 | 118, 122 | breqtrd 4029 |
. . . . . . . . . 10
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β€ (π + 1)) |
124 | 82 | adantr 276 |
. . . . . . . . . 10
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβ(β‘πβ(π + 1))) = (π + 1)) |
125 | 123, 124 | breqtrrd 4031 |
. . . . . . . . 9
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (πβdom (π»β(π + 1))) β€ (πβ(β‘πβ(π + 1)))) |
126 | 86 | adantr 276 |
. . . . . . . . . 10
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (β‘πβ(π + 1)) β Ο) |
127 | 113, 26, 114, 126 | frec2uzled 10428 |
. . . . . . . . 9
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β (dom (π»β(π + 1)) β (β‘πβ(π + 1)) β (πβdom (π»β(π + 1))) β€ (πβ(β‘πβ(π + 1))))) |
128 | 125, 127 | mpbird 167 |
. . . . . . . 8
β’ ((((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β§ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) β dom (π»β(π + 1)) β (β‘πβ(π + 1))) |
129 | 39, 40, 71 | ennnfonelemdc 12399 |
. . . . . . . . 9
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β DECID (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ))) |
130 | | exmiddc 836 |
. . . . . . . . 9
β’
(DECID (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)) β ((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)) β¨ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)))) |
131 | 129, 130 | syl 14 |
. . . . . . . 8
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β ((πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)) β¨ Β¬ (πΉβ(β‘πβπ)) β (πΉ β (β‘πβπ)))) |
132 | 89, 128, 131 | mpjaodan 798 |
. . . . . . 7
β’ (((π β§ π β (β€β₯β0))
β§ dom (π»βπ) β (β‘πβπ)) β dom (π»β(π + 1)) β (β‘πβ(π + 1))) |
133 | 132 | ex 115 |
. . . . . 6
β’ ((π β§ π β (β€β₯β0))
β (dom (π»βπ) β (β‘πβπ) β dom (π»β(π + 1)) β (β‘πβ(π + 1)))) |
134 | 133 | expcom 116 |
. . . . 5
β’ (π β
(β€β₯β0) β (π β (dom (π»βπ) β (β‘πβπ) β dom (π»β(π + 1)) β (β‘πβ(π + 1))))) |
135 | 134 | a2d 26 |
. . . 4
β’ (π β
(β€β₯β0) β ((π β dom (π»βπ) β (β‘πβπ)) β (π β dom (π»β(π + 1)) β (β‘πβ(π + 1))))) |
136 | 6, 11, 16, 21, 35, 135 | uzind4 9587 |
. . 3
β’ (π β
(β€β₯β0) β (π β dom (π»βπ) β (β‘πβπ))) |
137 | 136, 43 | eleq2s 2272 |
. 2
β’ (π β β0
β (π β dom (π»βπ) β (β‘πβπ))) |
138 | 1, 137 | mpcom 36 |
1
β’ (π β dom (π»βπ) β (β‘πβπ)) |