Theorem mpondm0

Description: The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017)

	Ref	Expression
Hypothesis	mpondm0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
Assertion	mpondm0	⊢ ( ¬ ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑉 𝐹 𝑊 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mpondm0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
2		df-mpo	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑧 = 𝐶 ) }
3	1 2	eqtri	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑧 = 𝐶 ) }
4	3	dmeqi	⊢ dom 𝐹 = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑧 = 𝐶 ) }
5		dmoprabss	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑧 = 𝐶 ) } ⊆ ( 𝑋 × 𝑌 )
6	4 5	eqsstri	⊢ dom 𝐹 ⊆ ( 𝑋 × 𝑌 )
7		nssdmovg	⊢ ( ( dom 𝐹 ⊆ ( 𝑋 × 𝑌 ) ∧ ¬ ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ) → ( 𝑉 𝐹 𝑊 ) = ∅ )
8	6 7	mpan	⊢ ( ¬ ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑉 𝐹 𝑊 ) = ∅ )