Theorem fixun

Description: The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	fixun	|- Fix ( A u. B ) = ( Fix A u. Fix B )

Proof

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 )