Step | Hyp | Ref
| Expression |
1 | | nninfsel.e |
. 2
β’ πΈ = (π β (2o
βπ ββ) β¦ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
2 | | nninfsellemcl 14763 |
. . . . 5
β’ ((π β (2o
βπ ββ) β§ π β Ο) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β 2o) |
3 | | eqid 2177 |
. . . . 5
β’ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
4 | 2, 3 | fmptd 5671 |
. . . 4
β’ (π β (2o
βπ ββ) β (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)):ΟβΆ2o) |
5 | | 2onn 6522 |
. . . . . 6
β’
2o β Ο |
6 | 5 | a1i 9 |
. . . . 5
β’ (π β (2o
βπ ββ) β 2o
β Ο) |
7 | | omex 4593 |
. . . . . 6
β’ Ο
β V |
8 | 7 | a1i 9 |
. . . . 5
β’ (π β (2o
βπ ββ) β Ο β
V) |
9 | 6, 8 | elmapd 6662 |
. . . 4
β’ (π β (2o
βπ ββ) β ((π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β (2o βπ
Ο) β (π β
Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)):ΟβΆ2o)) |
10 | 4, 9 | mpbird 167 |
. . 3
β’ (π β (2o
βπ ββ) β (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β (2o βπ
Ο)) |
11 | | nninfsellemsuc 14764 |
. . . . 5
β’ ((π β (2o
βπ ββ) β§ π β Ο) β if(βπ β suc suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
12 | | peano2 4595 |
. . . . . 6
β’ (π β Ο β suc π β
Ο) |
13 | | nninfsellemcl 14763 |
. . . . . . 7
β’ ((π β (2o
βπ ββ) β§ suc π β Ο) β
if(βπ β suc suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β 2o) |
14 | 12, 13 | sylan2 286 |
. . . . . 6
β’ ((π β (2o
βπ ββ) β§ π β Ο) β if(βπ β suc suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β 2o) |
15 | | suceq 4403 |
. . . . . . . . 9
β’ (π = suc π β suc π = suc suc π) |
16 | 15 | raleqdv 2679 |
. . . . . . . 8
β’ (π = suc π β (βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β βπ β suc
suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
17 | 16 | ifbid 3556 |
. . . . . . 7
β’ (π = suc π β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = if(βπ β suc suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
18 | 17, 3 | fvmptg 5593 |
. . . . . 6
β’ ((suc
π β Ο β§
if(βπ β suc suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β 2o) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) = if(βπ β suc suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
19 | 12, 14, 18 | syl2an2 594 |
. . . . 5
β’ ((π β (2o
βπ ββ) β§ π β Ο) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) = if(βπ β suc suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
20 | | simpr 110 |
. . . . . 6
β’ ((π β (2o
βπ ββ) β§ π β Ο) β π β Ο) |
21 | | nninfsellemcl 14763 |
. . . . . 6
β’ ((π β (2o
βπ ββ) β§ π β Ο) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β 2o) |
22 | | suceq 4403 |
. . . . . . . . 9
β’ (π = π β suc π = suc π) |
23 | 22 | raleqdv 2679 |
. . . . . . . 8
β’ (π = π β (βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
24 | 23 | ifbid 3556 |
. . . . . . 7
β’ (π = π β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
25 | 24, 3 | fvmptg 5593 |
. . . . . 6
β’ ((π β Ο β§
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β 2o) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
26 | 20, 21, 25 | syl2anc 411 |
. . . . 5
β’ ((π β (2o
βπ ββ) β§ π β Ο) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
27 | 11, 19, 26 | 3sstr4d 3201 |
. . . 4
β’ ((π β (2o
βπ ββ) β§ π β Ο) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ)) |
28 | 27 | ralrimiva 2550 |
. . 3
β’ (π β (2o
βπ ββ) β βπ β Ο ((π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ)) |
29 | | fveq1 5515 |
. . . . . 6
β’ (π = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β (πβsuc π) = ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π)) |
30 | | fveq1 5515 |
. . . . . 6
β’ (π = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β (πβπ) = ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ)) |
31 | 29, 30 | sseq12d 3187 |
. . . . 5
β’ (π = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β ((πβsuc π) β (πβπ) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ))) |
32 | 31 | ralbidv 2477 |
. . . 4
β’ (π = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β (βπ β Ο (πβsuc π) β (πβπ) β βπ β Ο ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ))) |
33 | | df-nninf 7119 |
. . . 4
β’
ββ = {π β (2o
βπ Ο) β£ βπ β Ο (πβsuc π) β (πβπ)} |
34 | 32, 33 | elrab2 2897 |
. . 3
β’ ((π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β ββ β ((π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β (2o βπ
Ο) β§ βπ
β Ο ((π β
Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βsuc π) β ((π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))βπ))) |
35 | 10, 28, 34 | sylanbrc 417 |
. 2
β’ (π β (2o
βπ ββ) β (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β ββ) |
36 | 1, 35 | fmpti 5669 |
1
β’ πΈ:(2o
βπ
ββ)βΆββ |