| Step |
Hyp |
Ref |
Expression |
| 1 |
|
indir |
|- ( ( A u. B ) i^i _I ) = ( ( A i^i _I ) u. ( B i^i _I ) ) |
| 2 |
1
|
dmeqi |
|- dom ( ( A u. B ) i^i _I ) = dom ( ( A i^i _I ) u. ( B i^i _I ) ) |
| 3 |
|
dmun |
|- dom ( ( A i^i _I ) u. ( B i^i _I ) ) = ( dom ( A i^i _I ) u. dom ( B i^i _I ) ) |
| 4 |
2 3
|
eqtri |
|- dom ( ( A u. B ) i^i _I ) = ( dom ( A i^i _I ) u. dom ( B i^i _I ) ) |
| 5 |
|
df-fix |
|- Fix ( A u. B ) = dom ( ( A u. B ) i^i _I ) |
| 6 |
|
df-fix |
|- Fix A = dom ( A i^i _I ) |
| 7 |
|
df-fix |
|- Fix B = dom ( B i^i _I ) |
| 8 |
6 7
|
uneq12i |
|- ( Fix A u. Fix B ) = ( dom ( A i^i _I ) u. dom ( B i^i _I ) ) |
| 9 |
4 5 8
|
3eqtr4i |
|- Fix ( A u. B ) = ( Fix A u. Fix B ) |