Theorem mpo0

Description: A mapping operation with empty domain. In this version of mpo0v , the class of the second operator may depend on the first operator. (Contributed by Stefan O'Rear, 29-Jan-2015) (Revised by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	mpo0	⊢ ( 𝑥 ∈ ∅ , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-mpo	⊢ ( 𝑥 ∈ ∅ , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
2		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
3		noel	⊢ ¬ 𝑥 ∈ ∅
4		simprll	⊢ ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) → 𝑥 ∈ ∅ )
5	3 4	mto	⊢ ¬ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) )
6	5	nex	⊢ ¬ ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) )
7	6	nex	⊢ ¬ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) )
8	7	nex	⊢ ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) )
9	8	abf	⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } = ∅
10	1 2 9	3eqtri	⊢ ( 𝑥 ∈ ∅ , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅