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	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1^st ‘ 𝑥 ) ↦ { 𝑛 ∈ ( 1^st ‘ 𝑥 ) ∣ 𝜑 } )
	mpoxopoveqd.1	⊢ ( 𝜓 → ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) )
	mpoxopoveqd.2	⊢ ( ( 𝜓 ∧ ¬ 𝐾 ∈ 𝑉 ) → { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } = ∅ )
Assertion	mpoxopoveqd	⊢ ( 𝜓 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		mpoxopoveq.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1^st ‘ 𝑥 ) ↦ { 𝑛 ∈ ( 1^st ‘ 𝑥 ) ∣ 𝜑 } )
2		mpoxopoveqd.1	⊢ ( 𝜓 → ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) )
3		mpoxopoveqd.2	⊢ ( ( 𝜓 ∧ ¬ 𝐾 ∈ 𝑉 ) → { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } = ∅ )
4	1	mpoxopoveq	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )
5	4	ex	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐾 ∈ 𝑉 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ) )
6	5 2	syl11	⊢ ( 𝐾 ∈ 𝑉 → ( 𝜓 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ) )
7		df-nel	⊢ ( 𝐾 ∉ 𝑉 ↔ ¬ 𝐾 ∈ 𝑉 )
8	1	mpoxopynvov0	⊢ ( 𝐾 ∉ 𝑉 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ )
9	7 8	sylbir	⊢ ( ¬ 𝐾 ∈ 𝑉 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ )
10	9	adantr	⊢ ( ( ¬ 𝐾 ∈ 𝑉 ∧ 𝜓 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ∅ )
11	3	eqcomd	⊢ ( ( 𝜓 ∧ ¬ 𝐾 ∈ 𝑉 ) → ∅ = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )
12	11	ancoms	⊢ ( ( ¬ 𝐾 ∈ 𝑉 ∧ 𝜓 ) → ∅ = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )
13	10 12	eqtrd	⊢ ( ( ¬ 𝐾 ∈ 𝑉 ∧ 𝜓 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )
14	13	ex	⊢ ( ¬ 𝐾 ∈ 𝑉 → ( 𝜓 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ) )
15	6 14	pm2.61i	⊢ ( 𝜓 → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )

Metamath Proof Explorer

Theorem mpoxopoveqd

Proof