Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
โข โ โ V |
2 |
1 1
|
elmap |
โข ( ๐ โ ( โ โm โ ) โ ๐ : โ โถ โ ) |
3 |
|
oveq1 |
โข ( ๐ = ๐ด โ ( ๐ ยทโ ( ๐ โ ๐ฅ ) ) = ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) |
4 |
3
|
mpteq2dv |
โข ( ๐ = ๐ด โ ( ๐ฅ โ โ โฆ ( ๐ ยทโ ( ๐ โ ๐ฅ ) ) ) = ( ๐ฅ โ โ โฆ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) ) |
5 |
|
fveq1 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ฅ ) = ( ๐ โ ๐ฅ ) ) |
6 |
5
|
oveq2d |
โข ( ๐ = ๐ โ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) = ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) |
7 |
6
|
mpteq2dv |
โข ( ๐ = ๐ โ ( ๐ฅ โ โ โฆ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) = ( ๐ฅ โ โ โฆ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) ) |
8 |
|
df-homul |
โข ยทop = ( ๐ โ โ , ๐ โ ( โ โm โ ) โฆ ( ๐ฅ โ โ โฆ ( ๐ ยทโ ( ๐ โ ๐ฅ ) ) ) ) |
9 |
1
|
mptex |
โข ( ๐ฅ โ โ โฆ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) โ V |
10 |
4 7 8 9
|
ovmpo |
โข ( ( ๐ด โ โ โง ๐ โ ( โ โm โ ) ) โ ( ๐ด ยทop ๐ ) = ( ๐ฅ โ โ โฆ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) ) |
11 |
2 10
|
sylan2br |
โข ( ( ๐ด โ โ โง ๐ : โ โถ โ ) โ ( ๐ด ยทop ๐ ) = ( ๐ฅ โ โ โฆ ( ๐ด ยทโ ( ๐ โ ๐ฅ ) ) ) ) |