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 ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
idresefmnd.e ⊢ 𝐸 = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
Assertion idresefmnd ( 𝐴 ∈ 𝑉 → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 idressubmefmnd.g ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 idresefmnd.e ⊢ 𝐸 = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
3 1 idressubmefmnd ⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) )
4 1 efmndmnd ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 eqid ⊢ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
8 5 6 7 issubm2 ⊢ ( 𝐺 ∈ Mnd → ( { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) ↔ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) ) )
9 4 8 syl ⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) ↔ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) ) )
10 snex ⊢ { ( I ↾ 𝐴 ) } ∈ V
11 2 5 ressbas ⊢ ( { ( I ↾ 𝐴 ) } ∈ V → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
12 10 11 mp1i ⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
13 inss2 ⊢ ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) ⊆ ( Base ‘ 𝐺 )
14 12 13 eqsstrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) )
15 2 eqcomi ⊢ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) = 𝐸
16 15 eleq1i ⊢ ( ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd ↔ 𝐸 ∈ Mnd )
17 16 biimpi ⊢ ( ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd → 𝐸 ∈ Mnd )
18 17 3ad2ant3 ⊢ ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) → 𝐸 ∈ Mnd )
19 14 18 anim12ci ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) ) → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )
20 19 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ { ( I ↾ 𝐴 ) } ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Mnd ) → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
21 9 20 sylbid ⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
22 3 21 mpd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ∈ Mnd ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )