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 ⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ 𝐵 ) )
Assertion elovmpt3imp ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )

Proof

Step Hyp Ref Expression
1 elovmpt3imp.o ⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ 𝐵 ) )
2 ne0i ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ≠ ∅ )
3 ax-1 ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ≠ ∅ → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
4 1 mpondm0 ⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 𝑂 𝑌 ) = ∅ )
5 fveq1 ⊢ ( ( 𝑋 𝑂 𝑌 ) = ∅ → ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) = ( ∅ ‘ 𝑍 ) )
6 0fv ⊢ ( ∅ ‘ 𝑍 ) = ∅
7 5 6 eqtrdi ⊢ ( ( 𝑋 𝑂 𝑌 ) = ∅ → ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) = ∅ )
8 eqneqall ⊢ ( ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) = ∅ → ( ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ≠ ∅ → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
9 4 7 8 3syl ⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ≠ ∅ → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
10 3 9 pm2.61i ⊢ ( ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) ≠ ∅ → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
11 2 10 syl ⊢ ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )