| Step |
Hyp |
Ref |
Expression |
| 1 |
|
scutval |
|- ( L < ( L |s R ) = ( iota_ x e. { y e. No | ( L < |
| 2 |
1
|
adantr |
|- ( ( L < ( L |s R ) = ( iota_ x e. { y e. No | ( L < |
| 3 |
|
sneq |
|- ( x = y -> { x } = { y } ) |
| 4 |
3
|
breq2d |
|- ( x = y -> ( L < L < |
| 5 |
3
|
breq1d |
|- ( x = y -> ( { x } < { y } < |
| 6 |
4 5
|
anbi12d |
|- ( x = y -> ( ( L < ( L < |
| 7 |
6
|
riotarab |
|- ( iota_ x e. { y e. No | ( L < |
| 8 |
2 7
|
eqtrdi |
|- ( ( L < ( L |s R ) = ( iota_ x e. No ( ( L < |
| 9 |
8
|
eqeq1d |
|- ( ( L < ( ( L |s R ) = X <-> ( iota_ x e. No ( ( L < |
| 10 |
|
conway |
|- ( L < E! x e. { y e. No | ( L < |
| 11 |
6
|
reurab |
|- ( E! x e. { y e. No | ( L < E! x e. No ( ( L < |
| 12 |
10 11
|
sylib |
|- ( L < E! x e. No ( ( L < |
| 13 |
|
df-3an |
|- ( ( L < ( ( L < |
| 14 |
|
sneq |
|- ( x = X -> { x } = { X } ) |
| 15 |
14
|
breq2d |
|- ( x = X -> ( L < L < |
| 16 |
14
|
breq1d |
|- ( x = X -> ( { x } < { X } < |
| 17 |
|
fveqeq2 |
|- ( x = X -> ( ( bday ` x ) = |^| ( bday " { y e. No | ( L < ( bday ` X ) = |^| ( bday " { y e. No | ( L < |
| 18 |
15 16 17
|
3anbi123d |
|- ( x = X -> ( ( L < ( L < |
| 19 |
13 18
|
bitr3id |
|- ( x = X -> ( ( ( L < ( L < |
| 20 |
19
|
riota2 |
|- ( ( X e. No /\ E! x e. No ( ( L < ( ( L < ( iota_ x e. No ( ( L < |
| 21 |
20
|
ancoms |
|- ( ( E! x e. No ( ( L < ( ( L < ( iota_ x e. No ( ( L < |
| 22 |
12 21
|
sylan |
|- ( ( L < ( ( L < ( iota_ x e. No ( ( L < |
| 23 |
9 22
|
bitr4d |
|- ( ( L < ( ( L |s R ) = X <-> ( L < |