| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-scut |
|- |s = ( a e. ~P No , b e. ( < ( iota_ x e. { y e. No | ( a < |
| 2 |
1
|
mpofun |
|- Fun |s |
| 3 |
|
dmscut |
|- dom |s = < |
| 4 |
|
df-fn |
|- ( |s Fn < ( Fun |s /\ dom |s = < |
| 5 |
2 3 4
|
mpbir2an |
|- |s Fn < |
| 6 |
1
|
rnmpo |
|- ran |s = { z | E. a e. ~P No E. b e. ( < |
| 7 |
|
vex |
|- a e. _V |
| 8 |
|
vex |
|- b e. _V |
| 9 |
7 8
|
elimasn |
|- ( b e. ( < <. a , b >. e. < |
| 10 |
|
df-br |
|- ( a < <. a , b >. e. < |
| 11 |
9 10
|
bitr4i |
|- ( b e. ( < a < |
| 12 |
|
scutval |
|- ( a < ( a |s b ) = ( iota_ x e. { y e. No | ( a < |
| 13 |
|
scutcl |
|- ( a < ( a |s b ) e. No ) |
| 14 |
12 13
|
eqeltrrd |
|- ( a < ( iota_ x e. { y e. No | ( a < |
| 15 |
11 14
|
sylbi |
|- ( b e. ( < ( iota_ x e. { y e. No | ( a < |
| 16 |
|
eleq1a |
|- ( ( iota_ x e. { y e. No | ( a < ( z = ( iota_ x e. { y e. No | ( a < z e. No ) ) |
| 17 |
15 16
|
syl |
|- ( b e. ( < ( z = ( iota_ x e. { y e. No | ( a < z e. No ) ) |
| 18 |
17
|
adantl |
|- ( ( a e. ~P No /\ b e. ( < ( z = ( iota_ x e. { y e. No | ( a < z e. No ) ) |
| 19 |
18
|
rexlimivv |
|- ( E. a e. ~P No E. b e. ( < z e. No ) |
| 20 |
19
|
abssi |
|- { z | E. a e. ~P No E. b e. ( < |
| 21 |
6 20
|
eqsstri |
|- ran |s C_ No |
| 22 |
|
df-f |
|- ( |s : < No <-> ( |s Fn < |
| 23 |
5 21 22
|
mpbir2an |
|- |s : < No |