| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssltex1 |
|- ( A < A e. _V ) |
| 2 |
|
ssltss1 |
|- ( A < A C_ No ) |
| 3 |
1 2
|
elpwd |
|- ( A < A e. ~P No ) |
| 4 |
|
df-br |
|- ( A < <. A , B >. e. < |
| 5 |
4
|
biimpi |
|- ( A < <. A , B >. e. < |
| 6 |
|
ssltex2 |
|- ( A < B e. _V ) |
| 7 |
|
elimasng |
|- ( ( A e. _V /\ B e. _V ) -> ( B e. ( < <. A , B >. e. < |
| 8 |
1 6 7
|
syl2anc |
|- ( A < ( B e. ( < <. A , B >. e. < |
| 9 |
5 8
|
mpbird |
|- ( A < B e. ( < |
| 10 |
|
riotaex |
|- ( iota_ x e. { y e. No | ( A < |
| 11 |
|
breq1 |
|- ( a = A -> ( a < A < |
| 12 |
|
breq2 |
|- ( b = B -> ( { y } < { y } < |
| 13 |
11 12
|
bi2anan9 |
|- ( ( a = A /\ b = B ) -> ( ( a < ( A < |
| 14 |
13
|
rabbidv |
|- ( ( a = A /\ b = B ) -> { y e. No | ( a < |
| 15 |
14
|
imaeq2d |
|- ( ( a = A /\ b = B ) -> ( bday " { y e. No | ( a < |
| 16 |
15
|
inteqd |
|- ( ( a = A /\ b = B ) -> |^| ( bday " { y e. No | ( a < |
| 17 |
16
|
eqeq2d |
|- ( ( a = A /\ b = B ) -> ( ( bday ` x ) = |^| ( bday " { y e. No | ( a < ( bday ` x ) = |^| ( bday " { y e. No | ( A < |
| 18 |
14 17
|
riotaeqbidv |
|- ( ( a = A /\ b = B ) -> ( iota_ x e. { y e. No | ( a < |
| 19 |
|
sneq |
|- ( a = A -> { a } = { A } ) |
| 20 |
19
|
imaeq2d |
|- ( a = A -> ( < |
| 21 |
|
df-scut |
|- |s = ( a e. ~P No , b e. ( < ( iota_ x e. { y e. No | ( a < |
| 22 |
18 20 21
|
ovmpox |
|- ( ( A e. ~P No /\ B e. ( < ( A |s B ) = ( iota_ x e. { y e. No | ( A < |
| 23 |
10 22
|
mp3an3 |
|- ( ( A e. ~P No /\ B e. ( < ( A |s B ) = ( iota_ x e. { y e. No | ( A < |
| 24 |
3 9 23
|
syl2anc |
|- ( A < ( A |s B ) = ( iota_ x e. { y e. No | ( A < |