Step | Hyp | Ref
| Expression |
1 | | fveq1 6824 |
. . . . . . 7
โข (๐ = ๐บ โ (๐โ๐ฆ) = (๐บโ๐ฆ)) |
2 | 1 | oveq2d 7353 |
. . . . . 6
โข (๐ = ๐บ โ (๐ ยท (๐โ๐ฆ)) = (๐ ยท (๐บโ๐ฆ))) |
3 | 2 | breq2d 5104 |
. . . . 5
โข (๐ = ๐บ โ ((๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) โ (๐โ๐ฆ) โค (๐ ยท (๐บโ๐ฆ)))) |
4 | 3 | ralbidv 3170 |
. . . 4
โข (๐ = ๐บ โ (โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐บโ๐ฆ)))) |
5 | 4 | 2rexbidv 3209 |
. . 3
โข (๐ = ๐บ โ (โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ)) โ โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐บโ๐ฆ)))) |
6 | 5 | rabbidv 3411 |
. 2
โข (๐ = ๐บ โ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))} = {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐บโ๐ฆ))}) |
7 | | df-bigo 46245 |
. 2
โข ฮ =
(๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |
8 | | ovex 7370 |
. . 3
โข (โ
โpm โ) โ V |
9 | 8 | rabex 5276 |
. 2
โข {๐ โ (โ
โpm โ) โฃ โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐บโ๐ฆ))} โ V |
10 | 6, 7, 9 | fvmpt 6931 |
1
โข (๐บ โ (โ
โpm โ) โ (ฮโ๐บ) = {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐บโ๐ฆ))}) |