Theorem mpoxneldm

Description: If the first argument of an operation given by a maps-to rule is not an element of the first component of the domain or the second argument is not an element of the second component of the domain depending on the first argument, then the value of the operation is the empty set. (Contributed by AV, 25-Oct-2020)

	Ref	Expression
Hypothesis	mpoxeldm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
Assertion	mpoxneldm	⊢ ( ( 𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) → ( 𝑋 𝐹 𝑌 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mpoxeldm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
2		df-nel	⊢ ( 𝑋 ∉ 𝐶 ↔ ¬ 𝑋 ∈ 𝐶 )
3		df-nel	⊢ ( 𝑌 ∉ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ↔ ¬ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 )
4	2 3	orbi12i	⊢ ( ( 𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) ↔ ( ¬ 𝑋 ∈ 𝐶 ∨ ¬ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) )
5		ianor	⊢ ( ¬ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) ↔ ( ¬ 𝑋 ∈ 𝐶 ∨ ¬ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) )
6	4 5	bitr4i	⊢ ( ( 𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) ↔ ¬ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) )
7		neq0	⊢ ( ¬ ( 𝑋 𝐹 𝑌 ) = ∅ ↔ ∃ 𝑛 𝑛 ∈ ( 𝑋 𝐹 𝑌 ) )
8	1	mpoxeldm	⊢ ( 𝑛 ∈ ( 𝑋 𝐹 𝑌 ) → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) )
9	8	exlimiv	⊢ ( ∃ 𝑛 𝑛 ∈ ( 𝑋 𝐹 𝑌 ) → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) )
10	7 9	sylbi	⊢ ( ¬ ( 𝑋 𝐹 𝑌 ) = ∅ → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) )
11	10	con1i	⊢ ( ¬ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) → ( 𝑋 𝐹 𝑌 ) = ∅ )
12	6 11	sylbi	⊢ ( ( 𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋ 𝑋 / 𝑥 ⦌ 𝐷 ) → ( 𝑋 𝐹 𝑌 ) = ∅ )