Theorem fixun

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

	Ref	Expression
Assertion	fixun	⊢ Fix ( 𝐴 ∪ 𝐵 ) = ( Fix 𝐴 ∪ Fix 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		indir	⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ I ) = ( ( 𝐴 ∩ I ) ∪ ( 𝐵 ∩ I ) )
2	1	dmeqi	⊢ dom ( ( 𝐴 ∪ 𝐵 ) ∩ I ) = dom ( ( 𝐴 ∩ I ) ∪ ( 𝐵 ∩ I ) )
3		dmun	⊢ dom ( ( 𝐴 ∩ I ) ∪ ( 𝐵 ∩ I ) ) = ( dom ( 𝐴 ∩ I ) ∪ dom ( 𝐵 ∩ I ) )
4	2 3	eqtri	⊢ dom ( ( 𝐴 ∪ 𝐵 ) ∩ I ) = ( dom ( 𝐴 ∩ I ) ∪ dom ( 𝐵 ∩ I ) )
5		df-fix	⊢ Fix ( 𝐴 ∪ 𝐵 ) = dom ( ( 𝐴 ∪ 𝐵 ) ∩ I )
6		df-fix	⊢ Fix 𝐴 = dom ( 𝐴 ∩ I )
7		df-fix	⊢ Fix 𝐵 = dom ( 𝐵 ∩ I )
8	6 7	uneq12i	⊢ ( Fix 𝐴 ∪ Fix 𝐵 ) = ( dom ( 𝐴 ∩ I ) ∪ dom ( 𝐵 ∩ I ) )
9	4 5 8	3eqtr4i	⊢ Fix ( 𝐴 ∪ 𝐵 ) = ( Fix 𝐴 ∪ Fix 𝐵 )