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

Metamath Proof Explorer

Theorem mpo0

Description: A mapping operation with empty domain. In this version of mpo0v , the class of the second operator may depend on the first operator. (Contributed by Stefan O'Rear, 29-Jan-2015) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion mpo0 
|- ( x e. (/) , y e. B |-> C ) = (/)

Proof

Step Hyp Ref Expression
1 df-mpo 
 |-  ( x e. (/) , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. (/) /\ y e. B ) /\ z = C ) }
2 df-oprab 
 |-  { <. <. x , y >. , z >. | ( ( x e. (/) /\ y e. B ) /\ z = C ) } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) ) }
3 noel 
 |-  -. x e. (/)
4 simprll 
 |-  ( ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) ) -> x e. (/) )
5 3 4 mto 
 |-  -. ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) )
6 5 nex 
 |-  -. E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) )
7 6 nex 
 |-  -. E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) )
8 7 nex 
 |-  -. E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) )
9 8 abf 
 |-  { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. (/) /\ y e. B ) /\ z = C ) ) } = (/)
10 1 2 9 3eqtri 
 |-  ( x e. (/) , y e. B |-> C ) = (/)