Description: Partial reverse closure for any structure defined as a two-argument function. (Contributed by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 2-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | strov2rcl.s | |- S = ( I F R ) |
|
| strov2rcl.b | |- B = ( Base ` S ) |
||
| strov2rcl.f | |- Rel dom F |
||
| Assertion | strov2rcl | |- ( X e. B -> I e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | strov2rcl.s | |- S = ( I F R ) |
|
| 2 | strov2rcl.b | |- B = ( Base ` S ) |
|
| 3 | strov2rcl.f | |- Rel dom F |
|
| 4 | 3 1 2 | elbasov | |- ( X e. B -> ( I e. _V /\ R e. _V ) ) |
| 5 | 4 | simpld | |- ( X e. B -> I e. _V ) |