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

Metamath Proof Explorer

Theorem mpoxopovel

Description: Element of the 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. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017)

Ref Expression
Hypothesis mpoxopoveq.f ⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ { 𝑛 ∈ ( 1st ‘ 𝑥 ) ∣ 𝜑 } )
Assertion mpoxopovel ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ↔ ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 mpoxopoveq.f ⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ { 𝑛 ∈ ( 1st ‘ 𝑥 ) ∣ 𝜑 } )
2 1 mpoxopn0yelv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → 𝐾 ∈ 𝑉 ) )
3 2 pm4.71rd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ↔ ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ) ) )
4 1 mpoxopoveq ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )
5 4 eleq2d ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ↔ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ) )
6 nfcv ⊢ Ⅎ 𝑛 𝑉
7 6 elrabsf ⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ↔ ( 𝑁 ∈ 𝑉 ∧ [ 𝑁 / 𝑛 ] [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ) )
8 sbccom ⊢ ( [ 𝑁 / 𝑛 ] [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝑁 / 𝑛 ] [ 𝐾 / 𝑦 ] 𝜑 )
9 sbccom ⊢ ( [ 𝑁 / 𝑛 ] [ 𝐾 / 𝑦 ] 𝜑 ↔ [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 )
10 9 sbcbii ⊢ ( [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝑁 / 𝑛 ] [ 𝐾 / 𝑦 ] 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 )
11 8 10 bitri ⊢ ( [ 𝑁 / 𝑛 ] [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 )
12 11 anbi2i ⊢ ( ( 𝑁 ∈ 𝑉 ∧ [ 𝑁 / 𝑛 ] [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ) ↔ ( 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) )
13 7 12 bitri ⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ↔ ( 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) )
14 5 13 bitrdi ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ↔ ( 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ) )
15 14 pm5.32da ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ) ↔ ( 𝐾 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ) ) )
16 3anass ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ↔ ( 𝐾 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ) )
17 15 16 bitr4di ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ) ↔ ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ) )
18 3 17 bitrd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) ↔ ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] [ 𝑁 / 𝑛 ] 𝜑 ) ) )