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