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 \in V, y \in V ⟼ (z \in M ⟼ B))$
	Assertion	elovmpt3imp	$⊢ A \in (X O Y) (Z) \to (X \in V \land Y \in V)$

Proof

Step	Hyp	Ref	Expression
1		elovmpt3imp.o	$⊢ O = (x \in V, y \in V ⟼ (z \in M ⟼ B))$
2		ne0i	$⊢ A \in (X O Y) (Z) \to (X O Y) (Z) \neq \emptyset$
3		ax-1	$⊢ (X \in V \land Y \in V) \to ((X O Y) (Z) \neq \emptyset \to (X \in V \land Y \in V))$
4	1	mpondm0	$⊢ \neg (X \in V \land Y \in V) \to X O Y = \emptyset$
5		fveq1	$⊢ X O Y = \emptyset \to (X O Y) (Z) = \emptyset (Z)$
6		0fv	$⊢ \emptyset (Z) = \emptyset$
7	5 6	eqtrdi	$⊢ X O Y = \emptyset \to (X O Y) (Z) = \emptyset$
8		eqneqall	$⊢ (X O Y) (Z) = \emptyset \to ((X O Y) (Z) \neq \emptyset \to (X \in V \land Y \in V))$
9	4 7 8	3syl	$⊢ \neg (X \in V \land Y \in V) \to ((X O Y) (Z) \neq \emptyset \to (X \in V \land Y \in V))$
10	3 9	pm2.61i	$⊢ (X O Y) (Z) \neq \emptyset \to (X \in V \land Y \in V)$
11	2 10	syl	$⊢ A \in (X O Y) (Z) \to (X \in V \land Y \in V)$

Metamath Proof Explorer

Theorem elovmpt3imp

Proof