Step | Hyp | Ref
| Expression |
1 | | nninfsel.e |
. . . . . . 7
β’ πΈ = (π β (2o
βπ ββ) β¦ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
2 | 1 | nninfself 14732 |
. . . . . 6
β’ πΈ:(2o
βπ
ββ)βΆββ |
3 | 2 | a1i 9 |
. . . . 5
β’ (π β πΈ:(2o βπ
ββ)βΆββ) |
4 | | nninfsel.q |
. . . . 5
β’ (π β π β (2o
βπ ββ)) |
5 | 3, 4 | ffvelcdmd 5652 |
. . . 4
β’ (π β (πΈβπ) β
ββ) |
6 | | nninff 7120 |
. . . 4
β’ ((πΈβπ) β ββ β
(πΈβπ):ΟβΆ2o) |
7 | 5, 6 | syl 14 |
. . 3
β’ (π β (πΈβπ):ΟβΆ2o) |
8 | 7 | ffnd 5366 |
. 2
β’ (π β (πΈβπ) Fn Ο) |
9 | | 1onn 6520 |
. . . . 5
β’
1o β Ο |
10 | | fnconstg 5413 |
. . . . 5
β’
(1o β Ο β (Ο Γ {1o})
Fn Ο) |
11 | 9, 10 | ax-mp 5 |
. . . 4
β’ (Ο
Γ {1o}) Fn Ο |
12 | | fconstmpt 4673 |
. . . . 5
β’ (Ο
Γ {1o}) = (π β Ο β¦
1o) |
13 | 12 | fneq1i 5310 |
. . . 4
β’ ((Ο
Γ {1o}) Fn Ο β (π β Ο β¦ 1o) Fn
Ο) |
14 | 11, 13 | mpbi 145 |
. . 3
β’ (π β Ο β¦
1o) Fn Ο |
15 | 14 | a1i 9 |
. 2
β’ (π β (π β Ο β¦ 1o) Fn
Ο) |
16 | | elequ2 2153 |
. . . . . . . . . 10
β’ (π = π β (π β π β π β π)) |
17 | 16 | ifbid 3555 |
. . . . . . . . 9
β’ (π = π β if(π β π, 1o, β
) = if(π β π, 1o, β
)) |
18 | 17 | mpteq2dv 4094 |
. . . . . . . 8
β’ (π = π β (π β Ο β¦ if(π β π, 1o, β
)) = (π β Ο β¦ if(π β π, 1o, β
))) |
19 | 18 | fveq2d 5519 |
. . . . . . 7
β’ (π = π β (πβ(π β Ο β¦ if(π β π, 1o, β
))) = (πβ(π β Ο β¦ if(π β π, 1o, β
)))) |
20 | 19 | eqeq1d 2186 |
. . . . . 6
β’ (π = π β ((πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
21 | 4 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β π β (2o
βπ ββ)) |
22 | | nninfsel.1 |
. . . . . . . . . 10
β’ (π β (πβ(πΈβπ)) = 1o) |
23 | 22 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β (πβ(πΈβπ)) = 1o) |
24 | | simpr 110 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β π β Ο) |
25 | 1, 21, 23, 24 | nninfsellemqall 14734 |
. . . . . . . 8
β’ ((π β§ π β Ο) β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
26 | 25 | ralrimiva 2550 |
. . . . . . 7
β’ (π β βπ β Ο (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
27 | 26 | ad2antrr 488 |
. . . . . 6
β’ (((π β§ π β Ο) β§ π β suc π) β βπ β Ο (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
28 | | simpr 110 |
. . . . . . 7
β’ (((π β§ π β Ο) β§ π β suc π) β π β suc π) |
29 | | peano2 4594 |
. . . . . . . 8
β’ (π β Ο β suc π β
Ο) |
30 | 29 | ad2antlr 489 |
. . . . . . 7
β’ (((π β§ π β Ο) β§ π β suc π) β suc π β Ο) |
31 | | elnn 4605 |
. . . . . . 7
β’ ((π β suc π β§ suc π β Ο) β π β Ο) |
32 | 28, 30, 31 | syl2anc 411 |
. . . . . 6
β’ (((π β§ π β Ο) β§ π β suc π) β π β Ο) |
33 | 20, 27, 32 | rspcdva 2846 |
. . . . 5
β’ (((π β§ π β Ο) β§ π β suc π) β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
34 | 33 | ralrimiva 2550 |
. . . 4
β’ ((π β§ π β Ο) β βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
35 | 34 | iftrued 3541 |
. . 3
β’ ((π β§ π β Ο) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = 1o) |
36 | | omex 4592 |
. . . . . . 7
β’ Ο
β V |
37 | 36 | mptex 5742 |
. . . . . 6
β’ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β V |
38 | 37 | a1i 9 |
. . . . 5
β’ ((π β§ π β Ο) β (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β V) |
39 | | fveq1 5514 |
. . . . . . . . . 10
β’ (π = π β (πβ(π β Ο β¦ if(π β π, 1o, β
))) = (πβ(π β Ο β¦ if(π β π, 1o, β
)))) |
40 | 39 | eqeq1d 2186 |
. . . . . . . . 9
β’ (π = π β ((πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
41 | 40 | ralbidv 2477 |
. . . . . . . 8
β’ (π = π β (βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
42 | 41 | ifbid 3555 |
. . . . . . 7
β’ (π = π β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
43 | 42 | mpteq2dv 4094 |
. . . . . 6
β’ (π = π β (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
44 | 43, 1 | fvmptg 5592 |
. . . . 5
β’ ((π β (2o
βπ ββ) β§ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β V) β (πΈβπ) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
45 | 21, 38, 44 | syl2anc 411 |
. . . 4
β’ ((π β§ π β Ο) β (πΈβπ) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
46 | | suceq 4402 |
. . . . . . 7
β’ (π = π β suc π = suc π) |
47 | 46 | adantl 277 |
. . . . . 6
β’ (((π β§ π β Ο) β§ π = π) β suc π = suc π) |
48 | 47 | raleqdv 2678 |
. . . . 5
β’ (((π β§ π β Ο) β§ π = π) β (βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
49 | 48 | ifbid 3555 |
. . . 4
β’ (((π β§ π β Ο) β§ π = π) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
50 | 35, 9 | eqeltrdi 2268 |
. . . 4
β’ ((π β§ π β Ο) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) β Ο) |
51 | 45, 49, 24, 50 | fvmptd 5597 |
. . 3
β’ ((π β§ π β Ο) β ((πΈβπ)βπ) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
52 | | eqidd 2178 |
. . . . . 6
β’ (π = π β 1o =
1o) |
53 | | eqid 2177 |
. . . . . 6
β’ (π β Ο β¦
1o) = (π β
Ο β¦ 1o) |
54 | 52, 53 | fvmptg 5592 |
. . . . 5
β’ ((π β Ο β§
1o β Ο) β ((π β Ο β¦
1o)βπ) =
1o) |
55 | 9, 54 | mpan2 425 |
. . . 4
β’ (π β Ο β ((π β Ο β¦
1o)βπ) =
1o) |
56 | 55 | adantl 277 |
. . 3
β’ ((π β§ π β Ο) β ((π β Ο β¦
1o)βπ) =
1o) |
57 | 35, 51, 56 | 3eqtr4d 2220 |
. 2
β’ ((π β§ π β Ο) β ((πΈβπ)βπ) = ((π β Ο β¦
1o)βπ)) |
58 | 8, 15, 57 | eqfnfvd 5616 |
1
β’ (π β (πΈβπ) = (π β Ο β¦
1o)) |