Theorem mpoxopynvov0g

Description: If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017)

	Ref	Expression
Hypothesis	mpoxopn0yelv.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ 𝐶 )
Assertion	mpoxopynvov0g	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∉ 𝑉 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mpoxopn0yelv.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ 𝐶 )
2		neq0	⊢ ( ¬ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ ↔ ∃ 𝑛 𝑛 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) )
3	1	mpoxopn0yelv	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑛 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → 𝐾 ∈ 𝑉 ) )
4		nnel	⊢ ( ¬ 𝐾 ∉ 𝑉 ↔ 𝐾 ∈ 𝑉 )
5	3 4	syl6ibr	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑛 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → ¬ 𝐾 ∉ 𝑉 ) )
6	5	exlimdv	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ∃ 𝑛 𝑛 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → ¬ 𝐾 ∉ 𝑉 ) )
7	2 6	syl5bi	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ¬ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ → ¬ 𝐾 ∉ 𝑉 ) )
8	7	con4d	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐾 ∉ 𝑉 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ ) )
9	8	imp	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∉ 𝑉 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ )