Metamath Proof Explorer


Theorem bj-pr2un

Description: The second projection preserves unions. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-pr2un pr2 ( 𝐴𝐵 ) = ( pr2 𝐴 ∪ pr2 𝐵 )

Proof

Step Hyp Ref Expression
1 bj-projun ( 1o Proj ( 𝐴𝐵 ) ) = ( ( 1o Proj 𝐴 ) ∪ ( 1o Proj 𝐵 ) )
2 df-bj-pr2 pr2 ( 𝐴𝐵 ) = ( 1o Proj ( 𝐴𝐵 ) )
3 df-bj-pr2 pr2 𝐴 = ( 1o Proj 𝐴 )
4 df-bj-pr2 pr2 𝐵 = ( 1o Proj 𝐵 )
5 3 4 uneq12i ( pr2 𝐴 ∪ pr2 𝐵 ) = ( ( 1o Proj 𝐴 ) ∪ ( 1o Proj 𝐵 ) )
6 1 2 5 3eqtr4i pr2 ( 𝐴𝐵 ) = ( pr2 𝐴 ∪ pr2 𝐵 )