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