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 ‘ 𝐺 ) ) |