Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
โข โ โ V |
2 |
1
|
elpw2 |
โข ( ๐ป โ ๐ซ โ โ ๐ป โ โ ) |
3 |
|
raleq |
โข ( ๐ง = ๐ป โ ( โ ๐ฆ โ ๐ง ( ๐ฅ ยทih ๐ฆ ) = 0 โ โ ๐ฆ โ ๐ป ( ๐ฅ ยทih ๐ฆ ) = 0 ) ) |
4 |
3
|
rabbidv |
โข ( ๐ง = ๐ป โ { ๐ฅ โ โ โฃ โ ๐ฆ โ ๐ง ( ๐ฅ ยทih ๐ฆ ) = 0 } = { ๐ฅ โ โ โฃ โ ๐ฆ โ ๐ป ( ๐ฅ ยทih ๐ฆ ) = 0 } ) |
5 |
|
df-oc |
โข โฅ = ( ๐ง โ ๐ซ โ โฆ { ๐ฅ โ โ โฃ โ ๐ฆ โ ๐ง ( ๐ฅ ยทih ๐ฆ ) = 0 } ) |
6 |
1
|
rabex |
โข { ๐ฅ โ โ โฃ โ ๐ฆ โ ๐ป ( ๐ฅ ยทih ๐ฆ ) = 0 } โ V |
7 |
4 5 6
|
fvmpt |
โข ( ๐ป โ ๐ซ โ โ ( โฅ โ ๐ป ) = { ๐ฅ โ โ โฃ โ ๐ฆ โ ๐ป ( ๐ฅ ยทih ๐ฆ ) = 0 } ) |
8 |
2 7
|
sylbir |
โข ( ๐ป โ โ โ ( โฅ โ ๐ป ) = { ๐ฅ โ โ โฃ โ ๐ฆ โ ๐ป ( ๐ฅ ยทih ๐ฆ ) = 0 } ) |