| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rightval |
Could not format ( _Right ` 1s ) = { x e. ( _Old ` ( bday ` 1s ) ) | 1s
|
| 2 |
|
bday1s |
Could not format ( bday ` 1s ) = 1o : No typesetting found for |- ( bday ` 1s ) = 1o with typecode |- |
| 3 |
2
|
fveq2i |
Could not format ( _Old ` ( bday ` 1s ) ) = ( _Old ` 1o ) : No typesetting found for |- ( _Old ` ( bday ` 1s ) ) = ( _Old ` 1o ) with typecode |- |
| 4 |
|
old1 |
Could not format ( _Old ` 1o ) = { 0s } : No typesetting found for |- ( _Old ` 1o ) = { 0s } with typecode |- |
| 5 |
3 4
|
eqtri |
Could not format ( _Old ` ( bday ` 1s ) ) = { 0s } : No typesetting found for |- ( _Old ` ( bday ` 1s ) ) = { 0s } with typecode |- |
| 6 |
5
|
rabeqi |
Could not format { x e. ( _Old ` ( bday ` 1s ) ) | 1s
|
| 7 |
|
breq2 |
Could not format ( x = 0s -> ( 1s 1s ( 1s 1s
|
| 8 |
7
|
rabsnif |
Could not format { x e. { 0s } | 1s
|
| 9 |
6 8
|
eqtri |
Could not format { x e. ( _Old ` ( bday ` 1s ) ) | 1s
|
| 10 |
|
0slt1s |
Could not format 0s
|
| 11 |
|
0sno |
Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |- |
| 12 |
|
1sno |
Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |- |
| 13 |
|
sltasym |
Could not format ( ( 0s e. No /\ 1s e. No ) -> ( 0s -. 1s ( 0s -. 1s
|
| 14 |
11 12 13
|
mp2an |
Could not format ( 0s -. 1s -. 1s
|
| 15 |
10 14
|
ax-mp |
Could not format -. 1s
|
| 16 |
15
|
iffalsei |
Could not format if ( 1s
|
| 17 |
1 9 16
|
3eqtri |
Could not format ( _Right ` 1s ) = (/) : No typesetting found for |- ( _Right ` 1s ) = (/) with typecode |- |