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