Description: Two ways of saying a function is a mapping of A to itself. (Contributed by AV, 27-Jan-2024) (Proof shortened by AV, 29-Mar-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | efmndbas.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
efmndbas.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | ||
Assertion | elefmndbas2 | ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efmndbas.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
2 | efmndbas.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
3 | 1 2 | efmndbasabf | ⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } |
4 | 3 | a1i | ⊢ ( 𝐹 ∈ 𝑉 → 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } ) |
5 | 4 | eleq2d | ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } ) ) |
6 | feq1 | ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴 ⟶ 𝐴 ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) | |
7 | eqid | ⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } | |
8 | 6 7 | elab2g | ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) |
9 | 5 8 | bitrd | ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) ) |