Metamath Proof Explorer


Theorem efmnd

Description: The monoid of endofunctions on set A . (Contributed by AV, 25-Jan-2024)

Ref Expression
Hypotheses efmnd.1
|- G = ( EndoFMnd ` A )
efmnd.2
|- B = ( A ^m A )
efmnd.3
|- .+ = ( f e. B , g e. B |-> ( f o. g ) )
efmnd.4
|- J = ( Xt_ ` ( A X. { ~P A } ) )
Assertion efmnd
|- ( A e. V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )

Proof

Step Hyp Ref Expression
1 efmnd.1
 |-  G = ( EndoFMnd ` A )
2 efmnd.2
 |-  B = ( A ^m A )
3 efmnd.3
 |-  .+ = ( f e. B , g e. B |-> ( f o. g ) )
4 efmnd.4
 |-  J = ( Xt_ ` ( A X. { ~P A } ) )
5 elex
 |-  ( A e. V -> A e. _V )
6 ovexd
 |-  ( a = A -> ( a ^m a ) e. _V )
7 id
 |-  ( b = ( a ^m a ) -> b = ( a ^m a ) )
8 id
 |-  ( a = A -> a = A )
9 8 8 oveq12d
 |-  ( a = A -> ( a ^m a ) = ( A ^m A ) )
10 9 2 eqtr4di
 |-  ( a = A -> ( a ^m a ) = B )
11 7 10 sylan9eqr
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> b = B )
12 11 opeq2d
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
13 eqidd
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> ( f o. g ) = ( f o. g ) )
14 11 11 13 mpoeq123dv
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> ( f e. b , g e. b |-> ( f o. g ) ) = ( f e. B , g e. B |-> ( f o. g ) ) )
15 14 3 eqtr4di
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> ( f e. b , g e. b |-> ( f o. g ) ) = .+ )
16 15 opeq2d
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. = <. ( +g ` ndx ) , .+ >. )
17 simpl
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> a = A )
18 pweq
 |-  ( a = A -> ~P a = ~P A )
19 18 sneqd
 |-  ( a = A -> { ~P a } = { ~P A } )
20 19 adantr
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> { ~P a } = { ~P A } )
21 17 20 xpeq12d
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> ( a X. { ~P a } ) = ( A X. { ~P A } ) )
22 21 fveq2d
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> ( Xt_ ` ( a X. { ~P a } ) ) = ( Xt_ ` ( A X. { ~P A } ) ) )
23 22 4 eqtr4di
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> ( Xt_ ` ( a X. { ~P a } ) ) = J )
24 23 opeq2d
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> <. ( TopSet ` ndx ) , ( Xt_ ` ( a X. { ~P a } ) ) >. = <. ( TopSet ` ndx ) , J >. )
25 12 16 24 tpeq123d
 |-  ( ( a = A /\ b = ( a ^m a ) ) -> { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( a X. { ~P a } ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
26 6 25 csbied
 |-  ( a = A -> [_ ( a ^m a ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( a X. { ~P a } ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
27 df-efmnd
 |-  EndoFMnd = ( a e. _V |-> [_ ( a ^m a ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( a X. { ~P a } ) ) >. } )
28 tpex
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } e. _V
29 26 27 28 fvmpt
 |-  ( A e. _V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
30 5 29 syl
 |-  ( A e. V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
31 1 30 eqtrid
 |-  ( A e. V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )