Description: If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | brovmptimex.mpt | |- F = ( x e. E , y e. G |-> H ) |
|
| brovmptimex.br | |- ( ph -> A R B ) |
||
| brovmptimex.ov | |- ( ph -> R = ( C F D ) ) |
||
| Assertion | brovmptimex | |- ( ph -> ( C e. _V /\ D e. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brovmptimex.mpt | |- F = ( x e. E , y e. G |-> H ) |
|
| 2 | brovmptimex.br | |- ( ph -> A R B ) |
|
| 3 | brovmptimex.ov | |- ( ph -> R = ( C F D ) ) |
|
| 4 | 3 2 | breqdi | |- ( ph -> A ( C F D ) B ) |
| 5 | brne0 | |- ( A ( C F D ) B -> ( C F D ) =/= (/) ) |
|
| 6 | 1 | reldmmpo | |- Rel dom F |
| 7 | 6 | ovprc | |- ( -. ( C e. _V /\ D e. _V ) -> ( C F D ) = (/) ) |
| 8 | 7 | necon1ai | |- ( ( C F D ) =/= (/) -> ( C e. _V /\ D e. _V ) ) |
| 9 | 4 5 8 | 3syl | |- ( ph -> ( C e. _V /\ D e. _V ) ) |