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 >. } ) |