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 ) )