Step |
Hyp |
Ref |
Expression |
1 |
|
istsr.1 |
|- X = dom R |
2 |
|
dmeq |
|- ( r = R -> dom r = dom R ) |
3 |
2 1
|
eqtr4di |
|- ( r = R -> dom r = X ) |
4 |
3
|
sqxpeqd |
|- ( r = R -> ( dom r X. dom r ) = ( X X. X ) ) |
5 |
|
id |
|- ( r = R -> r = R ) |
6 |
|
cnveq |
|- ( r = R -> `' r = `' R ) |
7 |
5 6
|
uneq12d |
|- ( r = R -> ( r u. `' r ) = ( R u. `' R ) ) |
8 |
4 7
|
sseq12d |
|- ( r = R -> ( ( dom r X. dom r ) C_ ( r u. `' r ) <-> ( X X. X ) C_ ( R u. `' R ) ) ) |
9 |
|
df-tsr |
|- TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) } |
10 |
8 9
|
elrab2 |
|- ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) ) |