Step |
Hyp |
Ref |
Expression |
1 |
|
opsrso.o |
|- O = ( ( I ordPwSer R ) ` T ) |
2 |
|
opsrso.i |
|- ( ph -> I e. V ) |
3 |
|
opsrso.r |
|- ( ph -> R e. Toset ) |
4 |
|
opsrso.t |
|- ( ph -> T C_ ( I X. I ) ) |
5 |
|
opsrso.w |
|- ( ph -> T We I ) |
6 |
|
opsrso.l |
|- .<_ = ( lt ` O ) |
7 |
|
opsrso.b |
|- B = ( Base ` O ) |
8 |
1 2 3 4 5
|
opsrtos |
|- ( ph -> O e. Toset ) |
9 |
|
eqid |
|- ( le ` O ) = ( le ` O ) |
10 |
7 9 6
|
tosso |
|- ( O e. Toset -> ( O e. Toset <-> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) ) ) |
11 |
10
|
ibi |
|- ( O e. Toset -> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) ) |
12 |
8 11
|
syl |
|- ( ph -> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) ) |
13 |
12
|
simpld |
|- ( ph -> .<_ Or B ) |