Step | Hyp | Ref
| Expression |
1 | | nninfsel.e |
. . . . 5
β’ πΈ = (π β (2o
βπ ββ) β¦ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
2 | 1 | nninfself 14765 |
. . . 4
β’ πΈ:(2o
βπ
ββ)βΆββ |
3 | 2 | a1i 9 |
. . 3
β’ (π β πΈ:(2o βπ
ββ)βΆββ) |
4 | | nninfsel.q |
. . 3
β’ (π β π β (2o
βπ ββ)) |
5 | 3, 4 | ffvelcdmd 5653 |
. 2
β’ (π β (πΈβπ) β
ββ) |
6 | | nninfsel.n |
. 2
β’ (π β π β Ο) |
7 | | fveq1 5515 |
. . . . . . . . . . 11
β’ (π = π β (πβ(π β Ο β¦ if(π β π, 1o, β
))) = (πβ(π β Ο β¦ if(π β π, 1o, β
)))) |
8 | 7 | eqeq1d 2186 |
. . . . . . . . . 10
β’ (π = π β ((πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
9 | 8 | ralbidv 2477 |
. . . . . . . . 9
β’ (π = π β (βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
10 | 9 | ifbid 3556 |
. . . . . . . 8
β’ (π = π β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) |
11 | 10 | mpteq2dv 4095 |
. . . . . . 7
β’ (π = π β (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
12 | | omex 4593 |
. . . . . . . 8
β’ Ο
β V |
13 | 12 | mptex 5743 |
. . . . . . 7
β’ (π β Ο β¦
if(βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
)) β V |
14 | 11, 1, 13 | fvmpt 5594 |
. . . . . 6
β’ (π β (2o
βπ ββ) β (πΈβπ) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
15 | 4, 14 | syl 14 |
. . . . 5
β’ (π β (πΈβπ) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
16 | 15 | adantr 276 |
. . . 4
β’ ((π β§ π β π) β (πΈβπ) = (π β Ο β¦ if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
))) |
17 | | simpr 110 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π = π) β π = π) |
18 | | simplr 528 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π = π) β π β π) |
19 | 17, 18 | eqeltrd 2254 |
. . . . . . 7
β’ (((π β§ π β π) β§ π = π) β π β π) |
20 | | nnord 4612 |
. . . . . . . . 9
β’ (π β Ο β Ord π) |
21 | | vex 2741 |
. . . . . . . . . 10
β’ π β V |
22 | | ordelsuc 4505 |
. . . . . . . . . 10
β’ ((π β V β§ Ord π) β (π β π β suc π β π)) |
23 | 21, 22 | mpan 424 |
. . . . . . . . 9
β’ (Ord
π β (π β π β suc π β π)) |
24 | 6, 20, 23 | 3syl 17 |
. . . . . . . 8
β’ (π β (π β π β suc π β π)) |
25 | 24 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ π β π) β§ π = π) β (π β π β suc π β π)) |
26 | 19, 25 | mpbid 147 |
. . . . . 6
β’ (((π β§ π β π) β§ π = π) β suc π β π) |
27 | | nninfsel.qk |
. . . . . . 7
β’ (π β βπ β π (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
28 | 27 | ad2antrr 488 |
. . . . . 6
β’ (((π β§ π β π) β§ π = π) β βπ β π (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
29 | | ssralv 3220 |
. . . . . 6
β’ (suc
π β π β (βπ β π (πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β βπ β suc
π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
30 | 26, 28, 29 | sylc 62 |
. . . . 5
β’ (((π β§ π β π) β§ π = π) β βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
31 | 30 | iftrued 3542 |
. . . 4
β’ (((π β§ π β π) β§ π = π) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = 1o) |
32 | | simpr 110 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
33 | 6 | adantr 276 |
. . . . 5
β’ ((π β§ π β π) β π β Ο) |
34 | | elnn 4606 |
. . . . 5
β’ ((π β π β§ π β Ο) β π β Ο) |
35 | 32, 33, 34 | syl2anc 411 |
. . . 4
β’ ((π β§ π β π) β π β Ο) |
36 | | 1onn 6521 |
. . . . 5
β’
1o β Ο |
37 | 36 | a1i 9 |
. . . 4
β’ ((π β§ π β π) β 1o β
Ο) |
38 | 16, 31, 35, 37 | fvmptd 5598 |
. . 3
β’ ((π β§ π β π) β ((πΈβπ)βπ) = 1o) |
39 | 38 | ralrimiva 2550 |
. 2
β’ (π β βπ β π ((πΈβπ)βπ) = 1o) |
40 | 21 | sucid 4418 |
. . . . . . 7
β’ π β suc π |
41 | 40 | a1i 9 |
. . . . . 6
β’ ((π β§ π = π) β π β suc π) |
42 | | 1n0 6433 |
. . . . . . . 8
β’
1o β β
|
43 | 42 | nesymi 2393 |
. . . . . . 7
β’ Β¬
β
= 1o |
44 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((π β§ π = π) β π = π) |
45 | 44 | eleq2d 2247 |
. . . . . . . . . . . 12
β’ ((π β§ π = π) β (π β π β π β π)) |
46 | 45 | ifbid 3556 |
. . . . . . . . . . 11
β’ ((π β§ π = π) β if(π β π, 1o, β
) = if(π β π, 1o, β
)) |
47 | 46 | mpteq2dv 4095 |
. . . . . . . . . 10
β’ ((π β§ π = π) β (π β Ο β¦ if(π β π, 1o, β
)) = (π β Ο β¦ if(π β π, 1o, β
))) |
48 | 47 | fveq2d 5520 |
. . . . . . . . 9
β’ ((π β§ π = π) β (πβ(π β Ο β¦ if(π β π, 1o, β
))) = (πβ(π β Ο β¦ if(π β π, 1o,
β
)))) |
49 | | nninfsel.qn |
. . . . . . . . . 10
β’ (π β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
β
) |
50 | 49 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π = π) β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
β
) |
51 | 48, 50 | eqtrd 2210 |
. . . . . . . 8
β’ ((π β§ π = π) β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
β
) |
52 | 51 | eqeq1d 2186 |
. . . . . . 7
β’ ((π β§ π = π) β ((πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β β
= 1o)) |
53 | 43, 52 | mtbiri 675 |
. . . . . 6
β’ ((π β§ π = π) β Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
54 | | elequ2 2153 |
. . . . . . . . . . . 12
β’ (π = π β (π β π β π β π)) |
55 | 54 | ifbid 3556 |
. . . . . . . . . . 11
β’ (π = π β if(π β π, 1o, β
) = if(π β π, 1o, β
)) |
56 | 55 | mpteq2dv 4095 |
. . . . . . . . . 10
β’ (π = π β (π β Ο β¦ if(π β π, 1o, β
)) = (π β Ο β¦ if(π β π, 1o, β
))) |
57 | 56 | fveq2d 5520 |
. . . . . . . . 9
β’ (π = π β (πβ(π β Ο β¦ if(π β π, 1o, β
))) = (πβ(π β Ο β¦ if(π β π, 1o, β
)))) |
58 | 57 | eqeq1d 2186 |
. . . . . . . 8
β’ (π = π β ((πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
59 | 58 | notbid 667 |
. . . . . . 7
β’ (π = π β (Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
60 | 59 | rspcev 2842 |
. . . . . 6
β’ ((π β suc π β§ Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o)
β βπ β suc
π Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
61 | 41, 53, 60 | syl2anc 411 |
. . . . 5
β’ ((π β§ π = π) β βπ β suc π Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
62 | | rexnalim 2466 |
. . . . 5
β’
(βπ β suc
π Β¬ (πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o
β Β¬ βπ
β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
63 | 61, 62 | syl 14 |
. . . 4
β’ ((π β§ π = π) β Β¬ βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
64 | 63 | iffalsed 3545 |
. . 3
β’ ((π β§ π = π) β if(βπ β suc π(πβ(π β Ο β¦ if(π β π, 1o, β
))) = 1o,
1o, β
) = β
) |
65 | | peano1 4594 |
. . . 4
β’ β
β Ο |
66 | 65 | a1i 9 |
. . 3
β’ (π β β
β
Ο) |
67 | 15, 64, 6, 66 | fvmptd 5598 |
. 2
β’ (π β ((πΈβπ)βπ) = β
) |
68 | 5, 6, 39, 67 | nnnninfeq 7126 |
1
β’ (π β (πΈβπ) = (π β Ο β¦ if(π β π, 1o, β
))) |