This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efmndcl

Description: The group operation of the monoid of endofunctions on A is closed. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndtset.g 
|- G = ( EndoFMnd ` A )
efmndplusg.b 
|- B = ( Base ` G )
efmndplusg.p 
|- .+ = ( +g ` G )
Assertion efmndcl 
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )

Proof

Step Hyp Ref Expression
1 efmndtset.g 
 |-  G = ( EndoFMnd ` A )
2 efmndplusg.b 
 |-  B = ( Base ` G )
3 efmndplusg.p 
 |-  .+ = ( +g ` G )
4 1 2 3 efmndov 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )
5 1 2 efmndbasf 
 |-  ( X e. B -> X : A --> A )
6 1 2 efmndbasf 
 |-  ( Y e. B -> Y : A --> A )
7 fco 
 |-  ( ( X : A --> A /\ Y : A --> A ) -> ( X o. Y ) : A --> A )
8 5 6 7 syl2an 
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) : A --> A )
9 coexg 
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )
10 1 2 elefmndbas2 
 |-  ( ( X o. Y ) e. _V -> ( ( X o. Y ) e. B <-> ( X o. Y ) : A --> A ) )
11 9 10 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( X o. Y ) e. B <-> ( X o. Y ) : A --> A ) )
12 8 11 mpbird 
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. B )
13 4 12 eqeltrd 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )