Theorem mpondm0

Description: The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017)

	Ref	Expression
Hypothesis	mpondm0.f	|- F = ( x e. X , y e. Y |-> C )
Assertion	mpondm0	|- ( -. ( V e. X /\ W e. Y ) -> ( V F W ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		mpondm0.f	|- F = ( x e. X , y e. Y |-> C )
2		df-mpo	|- ( x e. X , y e. Y |-> C ) = { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) }
3	1 2	eqtri	|- F = { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) }
4	3	dmeqi	|- dom F = dom { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) }
5		dmoprabss	|- dom { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) } C_ ( X X. Y )
6	4 5	eqsstri	|- dom F C_ ( X X. Y )
7		nssdmovg	|- ( ( dom F C_ ( X X. Y ) /\ -. ( V e. X /\ W e. Y ) ) -> ( V F W ) = (/) )
8	6 7	mpan	|- ( -. ( V e. X /\ W e. Y ) -> ( V F W ) = (/) )