Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
|- ( x = (/) -> ( (/) .o x ) = ( (/) .o (/) ) ) |
2 |
1
|
eqeq1d |
|- ( x = (/) -> ( ( (/) .o x ) = (/) <-> ( (/) .o (/) ) = (/) ) ) |
3 |
|
oveq2 |
|- ( x = y -> ( (/) .o x ) = ( (/) .o y ) ) |
4 |
3
|
eqeq1d |
|- ( x = y -> ( ( (/) .o x ) = (/) <-> ( (/) .o y ) = (/) ) ) |
5 |
|
oveq2 |
|- ( x = suc y -> ( (/) .o x ) = ( (/) .o suc y ) ) |
6 |
5
|
eqeq1d |
|- ( x = suc y -> ( ( (/) .o x ) = (/) <-> ( (/) .o suc y ) = (/) ) ) |
7 |
|
oveq2 |
|- ( x = A -> ( (/) .o x ) = ( (/) .o A ) ) |
8 |
7
|
eqeq1d |
|- ( x = A -> ( ( (/) .o x ) = (/) <-> ( (/) .o A ) = (/) ) ) |
9 |
|
0elon |
|- (/) e. On |
10 |
|
om0 |
|- ( (/) e. On -> ( (/) .o (/) ) = (/) ) |
11 |
9 10
|
ax-mp |
|- ( (/) .o (/) ) = (/) |
12 |
|
oveq1 |
|- ( ( (/) .o y ) = (/) -> ( ( (/) .o y ) +o (/) ) = ( (/) +o (/) ) ) |
13 |
|
oa0 |
|- ( (/) e. On -> ( (/) +o (/) ) = (/) ) |
14 |
9 13
|
ax-mp |
|- ( (/) +o (/) ) = (/) |
15 |
12 14
|
eqtrdi |
|- ( ( (/) .o y ) = (/) -> ( ( (/) .o y ) +o (/) ) = (/) ) |
16 |
|
peano1 |
|- (/) e. _om |
17 |
|
nnmsuc |
|- ( ( (/) e. _om /\ y e. _om ) -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) ) |
18 |
16 17
|
mpan |
|- ( y e. _om -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) ) |
19 |
18
|
eqeq1d |
|- ( y e. _om -> ( ( (/) .o suc y ) = (/) <-> ( ( (/) .o y ) +o (/) ) = (/) ) ) |
20 |
15 19
|
syl5ibr |
|- ( y e. _om -> ( ( (/) .o y ) = (/) -> ( (/) .o suc y ) = (/) ) ) |
21 |
2 4 6 8 11 20
|
finds |
|- ( A e. _om -> ( (/) .o A ) = (/) ) |