Step |
Hyp |
Ref |
Expression |
1 |
|
psref.1 |
|- X = dom R |
2 |
|
psdmrn |
|- ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) ) |
3 |
2
|
simpld |
|- ( R e. PosetRel -> dom R = U. U. R ) |
4 |
1 3
|
syl5eq |
|- ( R e. PosetRel -> X = U. U. R ) |
5 |
4
|
eleq2d |
|- ( R e. PosetRel -> ( A e. X <-> A e. U. U. R ) ) |
6 |
|
pslem |
|- ( R e. PosetRel -> ( ( ( A R A /\ A R A ) -> A R A ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R A /\ A R A ) -> A = A ) ) ) |
7 |
6
|
simp2d |
|- ( R e. PosetRel -> ( A e. U. U. R -> A R A ) ) |
8 |
5 7
|
sylbid |
|- ( R e. PosetRel -> ( A e. X -> A R A ) ) |
9 |
8
|
imp |
|- ( ( R e. PosetRel /\ A e. X ) -> A R A ) |