Description: The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | idressubmefmnd.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
| Assertion | idressubmefmnd | ⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idressubmefmnd.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
| 2 | 1 | efmndid | ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝐺 ) ) |
| 3 | 2 | sneqd | ⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } = { ( 0g ‘ 𝐺 ) } ) |
| 4 | 1 | efmndmnd | ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd ) |
| 5 | eqid | ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) | |
| 6 | 5 | 0subm | ⊢ ( 𝐺 ∈ Mnd → { ( 0g ‘ 𝐺 ) } ∈ ( SubMnd ‘ 𝐺 ) ) |
| 7 | 4 6 | syl | ⊢ ( 𝐴 ∈ 𝑉 → { ( 0g ‘ 𝐺 ) } ∈ ( SubMnd ‘ 𝐺 ) ) |
| 8 | 3 7 | eqeltrd | ⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) ) |