Step | Hyp | Ref
| Expression |
1 | | elfvdm 6922 |
. 2
โข (๐น โ (ฮโ๐บ) โ ๐บ โ dom ฮ) |
2 | | df-bigo 47514 |
. . . 4
โข ฮ =
(๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |
3 | 2 | dmeqi 5898 |
. . 3
โข dom
ฮ = dom (๐ โ
(โ โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) |
4 | | dmmptg 6235 |
. . . 4
โข
(โ๐ โ
(โ โpm โ){๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))} โ V โ dom (๐ โ (โ โpm โ)
โฆ {๐ โ (โ
โpm โ) โฃ โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) = (โ โpm
โ)) |
5 | | ovex 7438 |
. . . . . 6
โข (โ
โpm โ) โ V |
6 | 5 | rabex 5325 |
. . . . 5
โข {๐ โ (โ
โpm โ) โฃ โ๐ฅ โ โ โ๐ โ โ โ๐ฆ โ (dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))} โ V |
7 | 6 | a1i 11 |
. . . 4
โข (๐ โ (โ
โpm โ) โ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))} โ V) |
8 | 4, 7 | mprg 3061 |
. . 3
โข dom
(๐ โ (โ
โpm โ) โฆ {๐ โ (โ โpm โ)
โฃ โ๐ฅ โ
โ โ๐ โ
โ โ๐ฆ โ
(dom ๐ โฉ (๐ฅ[,)+โ))(๐โ๐ฆ) โค (๐ ยท (๐โ๐ฆ))}) = (โ โpm
โ) |
9 | 3, 8 | eqtri 2754 |
. 2
โข dom
ฮ = (โ โpm โ) |
10 | 1, 9 | eleqtrdi 2837 |
1
โข (๐น โ (ฮโ๐บ) โ ๐บ โ (โ โpm
โ)) |