Theorem aovmpt4g

Description: Value of a function given by the maps-to notation, analogous to ovmpt4g . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	aovmpt4g.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	aovmpt4g	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → (( 𝑥 𝐹 𝑦 )) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		aovmpt4g.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	dmmpog	⊢ ( 𝐶 ∈ 𝑉 → dom 𝐹 = ( 𝐴 × 𝐵 ) )
3		opelxpi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
4		eleq2	⊢ ( dom 𝐹 = ( 𝐴 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
5	3 4	imbitrrid	⊢ ( dom 𝐹 = ( 𝐴 × 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ) )
6	2 5	syl	⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ) )
7	6	impcom	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝐶 ∈ 𝑉 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 )
8	7	3impa	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 )
9	1	mpofun	⊢ Fun 𝐹
10		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ { ⟨ 𝑥 , 𝑦 ⟩ } ) )
11	9 10	ax-mp	⊢ Fun ( 𝐹 ↾ { ⟨ 𝑥 , 𝑦 ⟩ } )
12		df-dfat	⊢ ( 𝐹 defAt ⟨ 𝑥 , 𝑦 ⟩ ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ⟨ 𝑥 , 𝑦 ⟩ } ) ) )
13		aovfundmoveq	⊢ ( 𝐹 defAt ⟨ 𝑥 , 𝑦 ⟩ → (( 𝑥 𝐹 𝑦 )) = ( 𝑥 𝐹 𝑦 ) )
14	12 13	sylbir	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ⟨ 𝑥 , 𝑦 ⟩ } ) ) → (( 𝑥 𝐹 𝑦 )) = ( 𝑥 𝐹 𝑦 ) )
15	8 11 14	sylancl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → (( 𝑥 𝐹 𝑦 )) = ( 𝑥 𝐹 𝑦 ) )
16	1	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )
17	15 16	eqtrd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → (( 𝑥 𝐹 𝑦 )) = 𝐶 )