| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-0s |
|- 0s = ( (/) |s (/) ) |
| 2 |
1
|
fveq2i |
|- ( bday ` 0s ) = ( bday ` ( (/) |s (/) ) ) |
| 3 |
|
0elpw |
|- (/) e. ~P No |
| 4 |
|
nulssgt |
|- ( (/) e. ~P No -> (/) < |
| 5 |
|
scutbday |
|- ( (/) < ( bday ` ( (/) |s (/) ) ) = |^| ( bday " { x e. No | ( (/) < |
| 6 |
3 4 5
|
mp2b |
|- ( bday ` ( (/) |s (/) ) ) = |^| ( bday " { x e. No | ( (/) < |
| 7 |
2 6
|
eqtri |
|- ( bday ` 0s ) = |^| ( bday " { x e. No | ( (/) < |
| 8 |
|
snelpwi |
|- ( x e. No -> { x } e. ~P No ) |
| 9 |
|
nulsslt |
|- ( { x } e. ~P No -> (/) < |
| 10 |
|
nulssgt |
|- ( { x } e. ~P No -> { x } < |
| 11 |
9 10
|
jca |
|- ( { x } e. ~P No -> ( (/) < |
| 12 |
8 11
|
syl |
|- ( x e. No -> ( (/) < |
| 13 |
12
|
rabeqc |
|- { x e. No | ( (/) < |
| 14 |
|
bdaydm |
|- dom bday = No |
| 15 |
13 14
|
eqtr4i |
|- { x e. No | ( (/) < |
| 16 |
15
|
imaeq2i |
|- ( bday " { x e. No | ( (/) < |
| 17 |
|
imadmrn |
|- ( bday " dom bday ) = ran bday |
| 18 |
|
bdayrn |
|- ran bday = On |
| 19 |
16 17 18
|
3eqtri |
|- ( bday " { x e. No | ( (/) < |
| 20 |
19
|
inteqi |
|- |^| ( bday " { x e. No | ( (/) < |
| 21 |
|
inton |
|- |^| On = (/) |
| 22 |
7 20 21
|
3eqtri |
|- ( bday ` 0s ) = (/) |