This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑥 ∈ ∅ , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅