Theorem fixun

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

	Ref	Expression
Assertion	fixun	$$⊢\mathrm{𝖥𝗂𝗑}\left(A\cup B\right)=\mathrm{𝖥𝗂𝗑}A\cup \mathrm{𝖥𝗂𝗑}B$$

Proof

Step	Hyp	Ref	Expression
1		indir	$$⊢\left(A\cup B\right)\cap \mathrm{I}=\left(A\cap \mathrm{I}\right)\cup \left(B\cap \mathrm{I}\right)$$
2	1	dmeqi	$$⊢\mathrm{dom}\left(\left(A\cup B\right)\cap \mathrm{I}\right)=\mathrm{dom}\left(\left(A\cap \mathrm{I}\right)\cup \left(B\cap \mathrm{I}\right)\right)$$
3		dmun	$$⊢\mathrm{dom}\left(\left(A\cap \mathrm{I}\right)\cup \left(B\cap \mathrm{I}\right)\right)=\mathrm{dom}\left(A\cap \mathrm{I}\right)\cup \mathrm{dom}\left(B\cap \mathrm{I}\right)$$
4	2 3	eqtri	$$⊢\mathrm{dom}\left(\left(A\cup B\right)\cap \mathrm{I}\right)=\mathrm{dom}\left(A\cap \mathrm{I}\right)\cup \mathrm{dom}\left(B\cap \mathrm{I}\right)$$
5		df-fix	$$⊢\mathrm{𝖥𝗂𝗑}\left(A\cup B\right)=\mathrm{dom}\left(\left(A\cup B\right)\cap \mathrm{I}\right)$$
6		df-fix	$$⊢\mathrm{𝖥𝗂𝗑}A=\mathrm{dom}\left(A\cap \mathrm{I}\right)$$
7		df-fix	$$⊢\mathrm{𝖥𝗂𝗑}B=\mathrm{dom}\left(B\cap \mathrm{I}\right)$$
8	6 7	uneq12i	$$⊢\mathrm{𝖥𝗂𝗑}A\cup \mathrm{𝖥𝗂𝗑}B=\mathrm{dom}\left(A\cap \mathrm{I}\right)\cup \mathrm{dom}\left(B\cap \mathrm{I}\right)$$
9	4 5 8	3eqtr4i	$$⊢\mathrm{𝖥𝗂𝗑}\left(A\cup B\right)=\mathrm{𝖥𝗂𝗑}A\cup \mathrm{𝖥𝗂𝗑}B$$