This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 )