Theorem 1arympt1fv

Description: The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024)

	Ref	Expression
Hypothesis	1arympt1.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) )
Assertion	1arympt1fv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ { ⟨ 0 , 𝐵 ⟩ } ) = ( 𝐴 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		1arympt1.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) )
2	1	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ) )
3		fveq1	⊢ ( 𝑥 = { ⟨ 0 , 𝐵 ⟩ } → ( 𝑥 ‘ 0 ) = ( { ⟨ 0 , 𝐵 ⟩ } ‘ 0 ) )
4	3	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐵 ⟩ } ) → ( 𝑥 ‘ 0 ) = ( { ⟨ 0 , 𝐵 ⟩ } ‘ 0 ) )
5		c0ex	⊢ 0 ∈ V
6	5	a1i	⊢ ( 𝑋 ∈ 𝑉 → 0 ∈ V )
7	6	anim1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → ( 0 ∈ V ∧ 𝐵 ∈ 𝑋 ) )
8	7	adantr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐵 ⟩ } ) → ( 0 ∈ V ∧ 𝐵 ∈ 𝑋 ) )
9		fvsng	⊢ ( ( 0 ∈ V ∧ 𝐵 ∈ 𝑋 ) → ( { ⟨ 0 , 𝐵 ⟩ } ‘ 0 ) = 𝐵 )
10	8 9	syl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐵 ⟩ } ) → ( { ⟨ 0 , 𝐵 ⟩ } ‘ 0 ) = 𝐵 )
11	4 10	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐵 ⟩ } ) → ( 𝑥 ‘ 0 ) = 𝐵 )
12	11	fveq2d	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐵 ⟩ } ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) = ( 𝐴 ‘ 𝐵 ) )
13	5	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → 0 ∈ V )
14		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
15	13 14	fsnd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → { ⟨ 0 , 𝐵 ⟩ } : { 0 } ⟶ 𝑋 )
16		snex	⊢ { 0 } ∈ V
17	16	a1i	⊢ ( 𝐵 ∈ 𝑋 → { 0 } ∈ V )
18		elmapg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 0 } ∈ V ) → ( { ⟨ 0 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) ↔ { ⟨ 0 , 𝐵 ⟩ } : { 0 } ⟶ 𝑋 ) )
19	17 18	sylan2	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → ( { ⟨ 0 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) ↔ { ⟨ 0 , 𝐵 ⟩ } : { 0 } ⟶ 𝑋 ) )
20	15 19	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → { ⟨ 0 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) )
21		fvexd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ‘ 𝐵 ) ∈ V )
22	2 12 20 21	fvmptd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ { ⟨ 0 , 𝐵 ⟩ } ) = ( 𝐴 ‘ 𝐵 ) )