Metamath Proof Explorer


Theorem 1aryfvalel

Description: A unary (endo)function on a set X . (Contributed by AV, 15-May-2024)

Ref Expression
Assertion 1aryfvalel ( 𝑋𝑉 → ( 𝐹 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 1nn0 1 ∈ ℕ0
2 fzo01 ( 0 ..^ 1 ) = { 0 }
3 2 eqcomi { 0 } = ( 0 ..^ 1 )
4 3 naryfvalel ( ( 1 ∈ ℕ0𝑋𝑉 ) → ( 𝐹 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) )
5 1 4 mpan ( 𝑋𝑉 → ( 𝐹 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) )