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 syl5eq 
 |-  ( A e. V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )