This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = (/) )