Metamath Proof Explorer

Theorem idresefmnd

Description: The structure with the singleton containing only the identity function restricted to a set A as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on A to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on A . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses idressubmefmnd.g No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
idresefmnd.e ⊢ E = G ↾ 𝑠 I ↾ A
Assertion idresefmnd ⊢ A ∈ V → E ∈ Mnd ∧ Base E ⊆ Base G

Proof

Step Hyp Ref Expression
1 idressubmefmnd.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 idresefmnd.e ⊢ E = G ↾ 𝑠 I ↾ A
3 1 idressubmefmnd ⊢ A ∈ V → I ↾ A ∈ SubMnd ⁡ G
4 1 efmndmnd ⊢ A ∈ V → G ∈ Mnd
5 eqid ⊢ Base G = Base G
6 eqid ⊢ 0 G = 0 G
7 eqid ⊢ G ↾ 𝑠 I ↾ A = G ↾ 𝑠 I ↾ A
8 5 6 7 issubm2 ⊢ G ∈ Mnd → I ↾ A ∈ SubMnd ⁡ G ↔ I ↾ A ⊆ Base G ∧ 0 G ∈ I ↾ A ∧ G ↾ 𝑠 I ↾ A ∈ Mnd
9 4 8 syl ⊢ A ∈ V → I ↾ A ∈ SubMnd ⁡ G ↔ I ↾ A ⊆ Base G ∧ 0 G ∈ I ↾ A ∧ G ↾ 𝑠 I ↾ A ∈ Mnd
10 snex ⊢ I ↾ A ∈ V
11 2 5 ressbas ⊢ I ↾ A ∈ V → I ↾ A ∩ Base G = Base E
12 10 11 mp1i ⊢ A ∈ V → I ↾ A ∩ Base G = Base E
13 inss2 ⊢ I ↾ A ∩ Base G ⊆ Base G
14 12 13 eqsstrrdi ⊢ A ∈ V → Base E ⊆ Base G
15 2 eqcomi ⊢ G ↾ 𝑠 I ↾ A = E
16 15 eleq1i ⊢ G ↾ 𝑠 I ↾ A ∈ Mnd ↔ E ∈ Mnd
17 16 biimpi ⊢ G ↾ 𝑠 I ↾ A ∈ Mnd → E ∈ Mnd
18 17 3ad2ant3 ⊢ I ↾ A ⊆ Base G ∧ 0 G ∈ I ↾ A ∧ G ↾ 𝑠 I ↾ A ∈ Mnd → E ∈ Mnd
19 14 18 anim12ci ⊢ A ∈ V ∧ I ↾ A ⊆ Base G ∧ 0 G ∈ I ↾ A ∧ G ↾ 𝑠 I ↾ A ∈ Mnd → E ∈ Mnd ∧ Base E ⊆ Base G
20 19 ex ⊢ A ∈ V → I ↾ A ⊆ Base G ∧ 0 G ∈ I ↾ A ∧ G ↾ 𝑠 I ↾ A ∈ Mnd → E ∈ Mnd ∧ Base E ⊆ Base G
21 9 20 sylbid ⊢ A ∈ V → I ↾ A ∈ SubMnd ⁡ G → E ∈ Mnd ∧ Base E ⊆ Base G
22 3 21 mpd ⊢ A ∈ V → E ∈ Mnd ∧ Base E ⊆ Base G