Theorem mpoxopoveq

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

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

Proof

Step	Hyp	Ref	Expression
1		mpoxopoveq.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ { 𝑛 ∈ ( 1st ‘ 𝑥 ) ∣ 𝜑 } )
2	1	a1i	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ { 𝑛 ∈ ( 1st ‘ 𝑥 ) ∣ 𝜑 } ) )
3		fveq2	⊢ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) )
4		op1stg	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) = 𝑉 )
5	4	adantr	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) = 𝑉 )
6	3 5	sylan9eqr	⊢ ( ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) ∧ 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ) → ( 1st ‘ 𝑥 ) = 𝑉 )
7	6	adantrr	⊢ ( ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) ) → ( 1st ‘ 𝑥 ) = 𝑉 )
8		sbceq1a	⊢ ( 𝑦 = 𝐾 → ( 𝜑 ↔ [ 𝐾 / 𝑦 ] 𝜑 ) )
9	8	adantl	⊢ ( ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) → ( 𝜑 ↔ [ 𝐾 / 𝑦 ] 𝜑 ) )
10	9	adantl	⊢ ( ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) ) → ( 𝜑 ↔ [ 𝐾 / 𝑦 ] 𝜑 ) )
11		sbceq1a	⊢ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ → ( [ 𝐾 / 𝑦 ] 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ) )
12	11	adantr	⊢ ( ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) → ( [ 𝐾 / 𝑦 ] 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ) )
13	12	adantl	⊢ ( ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) ) → ( [ 𝐾 / 𝑦 ] 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ) )
14	10 13	bitrd	⊢ ( ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) ) → ( 𝜑 ↔ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 ) )
15	7 14	rabeqbidv	⊢ ( ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ ∧ 𝑦 = 𝐾 ) ) → { 𝑛 ∈ ( 1st ‘ 𝑥 ) ∣ 𝜑 } = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )
16		opex	⊢ ⟨ 𝑉 , 𝑊 ⟩ ∈ V
17	16	a1i	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ⟨ 𝑉 , 𝑊 ⟩ ∈ V )
18		simpr	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → 𝐾 ∈ 𝑉 )
19		rabexg	⊢ ( 𝑉 ∈ 𝑋 → { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ∈ V )
20	19	ad2antrr	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } ∈ V )
21		equid	⊢ 𝑧 = 𝑧
22		nfvd	⊢ ( 𝑧 = 𝑧 → Ⅎ 𝑥 ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) )
23	21 22	ax-mp	⊢ Ⅎ 𝑥 ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 )
24		nfvd	⊢ ( 𝑧 = 𝑧 → Ⅎ 𝑦 ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) )
25	21 24	ax-mp	⊢ Ⅎ 𝑦 ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 )
26		nfcv	⊢ Ⅎ 𝑦 ⟨ 𝑉 , 𝑊 ⟩
27		nfcv	⊢ Ⅎ 𝑥 𝐾
28		nfsbc1v	⊢ Ⅎ 𝑥 [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑
29		nfcv	⊢ Ⅎ 𝑥 𝑉
30	28 29	nfrabw	⊢ Ⅎ 𝑥 { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 }
31		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝐾 / 𝑦 ] 𝜑
32	26 31	nfsbcw	⊢ Ⅎ 𝑦 [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑
33		nfcv	⊢ Ⅎ 𝑦 𝑉
34	32 33	nfrabw	⊢ Ⅎ 𝑦 { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 }
35	2 15 6 17 18 20 23 25 26 27 30 34	ovmpodxf	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ 𝐾 ∈ 𝑉 ) → ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = { 𝑛 ∈ 𝑉 ∣ [ ⟨ 𝑉 , 𝑊 ⟩ / 𝑥 ] [ 𝐾 / 𝑦 ] 𝜑 } )