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

Metamath Proof Explorer

Theorem elovmpt3imp

Description: If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands must be sets. Remark: a function which is the result of an operation can be regared as operation with 3 operands - therefore the abbreviation "mpt3" is used in the label. (Contributed by AV, 16-May-2019)

Ref Expression
Hypothesis elovmpt3imp.o 
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> B ) )
Assertion elovmpt3imp 
|- ( A e. ( ( X O Y ) ` Z ) -> ( X e. _V /\ Y e. _V ) )

Proof

Step Hyp Ref Expression
1 elovmpt3imp.o 
 |-  O = ( x e. _V , y e. _V |-> ( z e. M |-> B ) )
2 ne0i 
 |-  ( A e. ( ( X O Y ) ` Z ) -> ( ( X O Y ) ` Z ) =/= (/) )
3 ax-1 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( ( ( X O Y ) ` Z ) =/= (/) -> ( X e. _V /\ Y e. _V ) ) )
4 1 mpondm0 
 |-  ( -. ( X e. _V /\ Y e. _V ) -> ( X O Y ) = (/) )
5 fveq1 
 |-  ( ( X O Y ) = (/) -> ( ( X O Y ) ` Z ) = ( (/) ` Z ) )
6 0fv 
 |-  ( (/) ` Z ) = (/)
7 5 6 eqtrdi 
 |-  ( ( X O Y ) = (/) -> ( ( X O Y ) ` Z ) = (/) )
8 eqneqall 
 |-  ( ( ( X O Y ) ` Z ) = (/) -> ( ( ( X O Y ) ` Z ) =/= (/) -> ( X e. _V /\ Y e. _V ) ) )
9 4 7 8 3syl 
 |-  ( -. ( X e. _V /\ Y e. _V ) -> ( ( ( X O Y ) ` Z ) =/= (/) -> ( X e. _V /\ Y e. _V ) ) )
10 3 9 pm2.61i 
 |-  ( ( ( X O Y ) ` Z ) =/= (/) -> ( X e. _V /\ Y e. _V ) )
11 2 10 syl 
 |-  ( A e. ( ( X O Y ) ` Z ) -> ( X e. _V /\ Y e. _V ) )