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	$⊢ (x \in \emptyset, y \in B ⟼ C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-mpo	$⊢ (x \in \emptyset, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in \emptyset \land y \in B) \land z = C)\}$
2		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in \emptyset \land y \in B) \land z = C)\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C))\}$
3		noel	$⊢ \neg x \in \emptyset$
4		simprll	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C)) \to x \in \emptyset$
5	3 4	mto	$⊢ \neg (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C))$
6	5	nex	$⊢ \neg \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C))$
7	6	nex	$⊢ \neg \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C))$
8	7	nex	$⊢ \neg \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C))$
9	8	abf	$⊢ \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in \emptyset \land y \in B) \land z = C))\} = \emptyset$
10	1 2 9	3eqtri	$⊢ (x \in \emptyset, y \in B ⟼ C) = \emptyset$