Step | Hyp | Ref
| Expression |
1 | | 0nn0 12433 |
. . . . 5
β’ 0 β
β0 |
2 | | iftrue 4493 |
. . . . . 6
β’ (π = 0 β if(π = 0, β
, (π β 1)) =
β
) |
3 | | eqid 2733 |
. . . . . 6
β’ (π β β0
β¦ if(π = 0, β
,
(π β 1))) = (π β β0
β¦ if(π = 0, β
,
(π β
1))) |
4 | | 0ex 5265 |
. . . . . 6
β’ β
β V |
5 | 2, 3, 4 | fvmpt 6949 |
. . . . 5
β’ (0 β
β0 β ((π β β0 β¦ if(π = 0, β
, (π β 1)))β0) =
β
) |
6 | 1, 5 | mp1i 13 |
. . . 4
β’ (π β ((π β β0 β¦ if(π = 0, β
, (π β 1)))β0) =
β
) |
7 | | 0elpw 5312 |
. . . 4
β’ β
β π« β0 |
8 | 6, 7 | eqeltrdi 2842 |
. . 3
β’ (π β ((π β β0 β¦ if(π = 0, β
, (π β 1)))β0) β
π« β0) |
9 | | df-ov 7361 |
. . . . 5
β’ (π₯(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))π¦) = ((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))ββ¨π₯, π¦β©) |
10 | | elpwi 4568 |
. . . . . . . . . . 11
β’ (π β π«
β0 β π β
β0) |
11 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π β π«
β0 β§ π
β β0) β π β
β0) |
12 | | ssrab2 4038 |
. . . . . . . . . 10
β’ {π β β0
β£ (π β π΄ β§ (π β π) β π΅)} β
β0 |
13 | | sadcl 16347 |
. . . . . . . . . 10
β’ ((π β β0
β§ {π β
β0 β£ (π β π΄ β§ (π β π) β π΅)} β β0) β
(π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β
β0) |
14 | 11, 12, 13 | sylancl 587 |
. . . . . . . . 9
β’ ((π β π«
β0 β§ π
β β0) β (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β
β0) |
15 | | nn0ex 12424 |
. . . . . . . . . 10
β’
β0 β V |
16 | 15 | elpw2 5303 |
. . . . . . . . 9
β’ ((π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β π« β0
β (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}) β
β0) |
17 | 14, 16 | sylibr 233 |
. . . . . . . 8
β’ ((π β π«
β0 β§ π
β β0) β (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β π«
β0) |
18 | 17 | rgen2 3191 |
. . . . . . 7
β’
βπ β
π« β0βπ β β0 (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β π«
β0 |
19 | | eqid 2733 |
. . . . . . . 8
β’ (π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) = (π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})) |
20 | 19 | fmpo 8001 |
. . . . . . 7
β’
(βπ β
π« β0βπ β β0 (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β π« β0
β (π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})):(π« β0 Γ
β0)βΆπ« β0) |
21 | 18, 20 | mpbi 229 |
. . . . . 6
β’ (π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})):(π« β0 Γ
β0)βΆπ« β0 |
22 | 21, 7 | f0cli 7049 |
. . . . 5
β’ ((π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}))ββ¨π₯, π¦β©) β π«
β0 |
23 | 9, 22 | eqeltri 2830 |
. . . 4
β’ (π₯(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))π¦) β π«
β0 |
24 | 23 | a1i 11 |
. . 3
β’ ((π β§ (π₯ β π« β0 β§
π¦ β V)) β (π₯(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))π¦) β π«
β0) |
25 | | nn0uz 12810 |
. . 3
β’
β0 = (β€β₯β0) |
26 | | 0zd 12516 |
. . 3
β’ (π β 0 β
β€) |
27 | | fvexd 6858 |
. . 3
β’ ((π β§ π₯ β (β€β₯β(0 +
1))) β ((π β
β0 β¦ if(π = 0, β
, (π β 1)))βπ₯) β V) |
28 | 8, 24, 25, 26, 27 | seqf2 13933 |
. 2
β’ (π β seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β
1)))):β0βΆπ«
β0) |
29 | | smuval.p |
. . 3
β’ π = seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1)))) |
30 | 29 | feq1i 6660 |
. 2
β’ (π:β0βΆπ«
β0 β seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β
1)))):β0βΆπ«
β0) |
31 | 28, 30 | sylibr 233 |
1
β’ (π β π:β0βΆπ«
β0) |