mpoxopoveqd

Description: Value 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, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017)

	Ref	Expression
Hypotheses	mpoxopoveq.f	$⊢ F = (x \in V, y \in 1^{st} (x) ⟼ \{n \in 1^{st} (x) \| φ\})$
	mpoxopoveqd.1	$⊢ ψ \to (V \in X \land W \in Y)$
	mpoxopoveqd.2	$⊢ (ψ \land \neg K \in V) \to \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\} = \emptyset$
Assertion	mpoxopoveqd	$⊢ ψ \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\}$

Proof

Step	Hyp	Ref	Expression
1		mpoxopoveq.f	$⊢ F = (x \in V, y \in 1^{st} (x) ⟼ \{n \in 1^{st} (x) \| φ\})$
2		mpoxopoveqd.1	$⊢ ψ \to (V \in X \land W \in Y)$
3		mpoxopoveqd.2	$⊢ (ψ \land \neg K \in V) \to \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\} = \emptyset$
4	1	mpoxopoveq	$⊢ ((V \in X \land W \in Y) \land K \in V) \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\}$
5	4	ex	$⊢ (V \in X \land W \in Y) \to (K \in V \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\})$
6	5 2	syl11	$⊢ K \in V \to (ψ \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\})$
7		df-nel	$⊢ K \notin V \leftrightarrow \neg K \in V$
8	1	mpoxopynvov0	$⊢ K \notin V \to ⟨V, W⟩ F K = \emptyset$
9	7 8	sylbir	$⊢ \neg K \in V \to ⟨V, W⟩ F K = \emptyset$
10	9	adantr	$⊢ (\neg K \in V \land ψ) \to ⟨V, W⟩ F K = \emptyset$
11	3	eqcomd	$⊢ (ψ \land \neg K \in V) \to \emptyset = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\}$
12	11	ancoms	$⊢ (\neg K \in V \land ψ) \to \emptyset = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\}$
13	10 12	eqtrd	$⊢ (\neg K \in V \land ψ) \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\}$
14	13	ex	$⊢ \neg K \in V \to (ψ \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\})$
15	6 14	pm2.61i	$⊢ ψ \to ⟨V, W⟩ F K = \{n \in V \| \underset{˙}{[} ⟨V, W⟩ / x \underset{˙}{]} \underset{˙}{[} K / y \underset{˙}{]} φ\}$

Metamath Proof Explorer

Theorem mpoxopoveqd

Proof