Description: The mapping of unary (endo)functions is a one-to-one function onto the set of endofunctions. (Contributed by AV, 19-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 1arymaptfv.h | ⊢ 𝐻 = ( ℎ ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 } ) ) ) | |
Assertion | 1arymaptf1o | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1arymaptfv.h | ⊢ 𝐻 = ( ℎ ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 } ) ) ) | |
2 | 1 | 1arymaptf1 | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m 𝑋 ) ) |
3 | 1 | 1arymaptfo | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m 𝑋 ) ) |
4 | df-f1o | ⊢ ( 𝐻 : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ↔ ( 𝐻 : ( 1 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m 𝑋 ) ∧ 𝐻 : ( 1 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m 𝑋 ) ) ) | |
5 | 2 3 4 | sylanbrc | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m 𝑋 ) ) |