Description: Domain of an operation given by the maps-to notation, closed form of dmmpo . Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017) (Proof shortened by AV, 10-Feb-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dmmpog.f | |- F = ( x e. A , y e. B |-> C ) |
|
| Assertion | dmmpog | |- ( C e. V -> dom F = ( A X. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmmpog.f | |- F = ( x e. A , y e. B |-> C ) |
|
| 2 | simpl | |- ( ( C e. V /\ ( x e. A /\ y e. B ) ) -> C e. V ) |
|
| 3 | 2 | ralrimivva | |- ( C e. V -> A. x e. A A. y e. B C e. V ) |
| 4 | 1 | dmmpoga | |- ( A. x e. A A. y e. B C e. V -> dom F = ( A X. B ) ) |
| 5 | 3 4 | syl | |- ( C e. V -> dom F = ( A X. B ) ) |