Theorem 1arympt1

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

	Ref	Expression
Hypothesis	1arympt1.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) )
Assertion	1arympt1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 : 𝑋 ⟶ 𝑋 ) → 𝐹 ∈ ( 1 -aryF 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		1arympt1.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) )
2		eqid	⊢ ( 𝑋 ↑m { 0 } ) = ( 𝑋 ↑m { 0 } )
3		id	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) → 𝑥 ∈ ( 𝑋 ↑m { 0 } ) )
4		c0ex	⊢ 0 ∈ V
5	4	snid	⊢ 0 ∈ { 0 }
6	5	a1i	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) → 0 ∈ { 0 } )
7	2 3 6	mapfvd	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) → ( 𝑥 ‘ 0 ) ∈ 𝑋 )
8		ffvelcdm	⊢ ( ( 𝐴 : 𝑋 ⟶ 𝑋 ∧ ( 𝑥 ‘ 0 ) ∈ 𝑋 ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ∈ 𝑋 )
9	7 8	sylan2	⊢ ( ( 𝐴 : 𝑋 ⟶ 𝑋 ∧ 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ∈ 𝑋 )
10	9 1	fmptd	⊢ ( 𝐴 : 𝑋 ⟶ 𝑋 → 𝐹 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 )
11		1aryfvalel	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) )
12	10 11	imbitrrid	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐴 : 𝑋 ⟶ 𝑋 → 𝐹 ∈ ( 1 -aryF 𝑋 ) ) )
13	12	imp	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 : 𝑋 ⟶ 𝑋 ) → 𝐹 ∈ ( 1 -aryF 𝑋 ) )