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 ∈ V , y ∈ V ⟼ z ∈ M ⟼ B
Assertion elovmpt3imp ⊢ A ∈ X O Y ⁡ Z → X ∈ V ∧ Y ∈ V

Proof

Step Hyp Ref Expression
1 elovmpt3imp.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ M ⟼ B
2 ne0i ⊢ A ∈ X O Y ⁡ Z → X O Y ⁡ Z ≠ ∅
3 ax-1 ⊢ X ∈ V ∧ Y ∈ V → X O Y ⁡ Z ≠ ∅ → X ∈ V ∧ Y ∈ V
4 1 mpondm0 ⊢ ¬ X ∈ V ∧ Y ∈ 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 ∈ V ∧ Y ∈ V
9 4 7 8 3syl ⊢ ¬ X ∈ V ∧ Y ∈ V → X O Y ⁡ Z ≠ ∅ → X ∈ V ∧ Y ∈ V
10 3 9 pm2.61i ⊢ X O Y ⁡ Z ≠ ∅ → X ∈ V ∧ Y ∈ V
11 2 10 syl ⊢ A ∈ X O Y ⁡ Z → X ∈ V ∧ Y ∈ V