| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssltbday.1 |
|- ( ph -> A = ( L |s R ) ) |
| 2 |
|
ssltbday.2 |
|- ( ph -> B e. No ) |
| 3 |
|
ssltbday.3 |
|- ( ph -> L < |
| 4 |
|
ssltbday.4 |
|- ( ph -> { B } < |
| 5 |
1
|
fveq2d |
|- ( ph -> ( bday ` A ) = ( bday ` ( L |s R ) ) ) |
| 6 |
2
|
snn0d |
|- ( ph -> { B } =/= (/) ) |
| 7 |
|
sslttr |
|- ( ( L < L < |
| 8 |
3 4 6 7
|
syl3anc |
|- ( ph -> L < |
| 9 |
|
scutbday |
|- ( L < ( bday ` ( L |s R ) ) = |^| ( bday " { x e. No | ( L < |
| 10 |
8 9
|
syl |
|- ( ph -> ( bday ` ( L |s R ) ) = |^| ( bday " { x e. No | ( L < |
| 11 |
|
bdayfn |
|- bday Fn No |
| 12 |
|
ssrab2 |
|- { x e. No | ( L < |
| 13 |
|
sneq |
|- ( x = B -> { x } = { B } ) |
| 14 |
13
|
breq2d |
|- ( x = B -> ( L < L < |
| 15 |
13
|
breq1d |
|- ( x = B -> ( { x } < { B } < |
| 16 |
14 15
|
anbi12d |
|- ( x = B -> ( ( L < ( L < |
| 17 |
3 4
|
jca |
|- ( ph -> ( L < |
| 18 |
16 2 17
|
elrabd |
|- ( ph -> B e. { x e. No | ( L < |
| 19 |
|
fnfvima |
|- ( ( bday Fn No /\ { x e. No | ( L < ( bday ` B ) e. ( bday " { x e. No | ( L < |
| 20 |
11 12 18 19
|
mp3an12i |
|- ( ph -> ( bday ` B ) e. ( bday " { x e. No | ( L < |
| 21 |
|
intss1 |
|- ( ( bday ` B ) e. ( bday " { x e. No | ( L < |^| ( bday " { x e. No | ( L < |
| 22 |
20 21
|
syl |
|- ( ph -> |^| ( bday " { x e. No | ( L < |
| 23 |
10 22
|
eqsstrd |
|- ( ph -> ( bday ` ( L |s R ) ) C_ ( bday ` B ) ) |
| 24 |
5 23
|
eqsstrd |
|- ( ph -> ( bday ` A ) C_ ( bday ` B ) ) |