fixun

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

		Ref	Expression
	Assertion	fixun	$⊢ 𝖥𝗂𝗑 (A \cup B) = 𝖥𝗂𝗑 A \cup 𝖥𝗂𝗑 B$

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

Metamath Proof Explorer