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 } ) ⟶ 𝑋 ) )