Metamath Proof Explorer


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 ffvelrn ( ( 𝐴 : 𝑋𝑋 ∧ ( 𝑥 ‘ 0 ) ∈ 𝑋 ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ∈ 𝑋 )
9 7 8 sylan2 ( ( 𝐴 : 𝑋𝑋𝑥 ∈ ( 𝑋m { 0 } ) ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ∈ 𝑋 )
10 9 1 fmptd ( 𝐴 : 𝑋𝑋𝐹 : ( 𝑋m { 0 } ) ⟶ 𝑋 )
11 1aryfvalel ( 𝑋𝑉 → ( 𝐹 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) )
12 10 11 syl5ibr ( 𝑋𝑉 → ( 𝐴 : 𝑋𝑋𝐹 ∈ ( 1 -aryF 𝑋 ) ) )
13 12 imp ( ( 𝑋𝑉𝐴 : 𝑋𝑋 ) → 𝐹 ∈ ( 1 -aryF 𝑋 ) )