Description: Two ways of saying a function is a mapping of A to itself. (Contributed by AV, 27-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | efmndbas.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
efmndbas.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | ||
Assertion | elefmndbas | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efmndbas.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
2 | efmndbas.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
3 | 1 2 | efmndbas | ⊢ 𝐵 = ( 𝐴 ↑m 𝐴 ) |
4 | 3 | eleq2i | ⊢ ( 𝐹 ∈ 𝐵 ↔ 𝐹 ∈ ( 𝐴 ↑m 𝐴 ) ) |
5 | id | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 ) | |
6 | 5 5 | elmapd | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ ( 𝐴 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) |
7 | 4 6 | syl5bb | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) |