| Step |
Hyp |
Ref |
Expression |
| 1 |
|
etasslt |
|- ( ( A < E. x e. No ( A < |
| 2 |
|
simpl1 |
|- ( ( ( A < A < |
| 3 |
|
scutbday |
|- ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A < |
| 4 |
2 3
|
syl |
|- ( ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A < |
| 5 |
|
bdayfn |
|- bday Fn No |
| 6 |
|
ssrab2 |
|- { y e. No | ( A < |
| 7 |
|
sneq |
|- ( y = x -> { y } = { x } ) |
| 8 |
7
|
breq2d |
|- ( y = x -> ( A < A < |
| 9 |
7
|
breq1d |
|- ( y = x -> ( { y } < { x } < |
| 10 |
8 9
|
anbi12d |
|- ( y = x -> ( ( A < ( A < |
| 11 |
|
simprl |
|- ( ( ( A < x e. No ) |
| 12 |
|
simprr1 |
|- ( ( ( A < A < |
| 13 |
|
simprr2 |
|- ( ( ( A < { x } < |
| 14 |
12 13
|
jca |
|- ( ( ( A < ( A < |
| 15 |
10 11 14
|
elrabd |
|- ( ( ( A < x e. { y e. No | ( A < |
| 16 |
|
fnfvima |
|- ( ( bday Fn No /\ { y e. No | ( A < ( bday ` x ) e. ( bday " { y e. No | ( A < |
| 17 |
5 6 15 16
|
mp3an12i |
|- ( ( ( A < ( bday ` x ) e. ( bday " { y e. No | ( A < |
| 18 |
|
intss1 |
|- ( ( bday ` x ) e. ( bday " { y e. No | ( A < |^| ( bday " { y e. No | ( A < |
| 19 |
17 18
|
syl |
|- ( ( ( A < |^| ( bday " { y e. No | ( A < |
| 20 |
4 19
|
eqsstrd |
|- ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` x ) ) |
| 21 |
|
simprr3 |
|- ( ( ( A < ( bday ` x ) C_ O ) |
| 22 |
20 21
|
sstrd |
|- ( ( ( A < ( bday ` ( A |s B ) ) C_ O ) |
| 23 |
1 22
|
rexlimddv |
|- ( ( A < ( bday ` ( A |s B ) ) C_ O ) |