Theorem dmmpog

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=\left(x\in A,y\in B⟼C\right)$$
Assertion	dmmpog	$$⊢C\in V\to \mathrm{dom}F=A\times B$$

Proof

Step	Hyp	Ref	Expression
1		dmmpog.f	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
2		simpl	$$⊢\left(C\in V\wedge \left(x\in A\wedge y\in B\right)\right)\to C\in V$$
3	2	ralrimivva	$$⊢C\in V\to \forall x\in A\forall y\in BC\in V$$
4	1	dmmpoga	$$⊢\forall x\in A\forall y\in BC\in V\to \mathrm{dom}F=A\times B$$
5	3 4	syl	$$⊢C\in V\to \mathrm{dom}F=A\times B$$