Theorem bj-projun

Description: The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-projun	|- ( A Proj ( B u. C ) ) = ( ( A Proj B ) u. ( A Proj C ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-proj	|- ( A Proj B ) = { x | { x } e. ( B " { A } ) }
2	1	abeq2i	|- ( x e. ( A Proj B ) <-> { x } e. ( B " { A } ) )
3		df-bj-proj	|- ( A Proj C ) = { x | { x } e. ( C " { A } ) }
4	3	abeq2i	|- ( x e. ( A Proj C ) <-> { x } e. ( C " { A } ) )
5	2 4	orbi12i	|- ( ( x e. ( A Proj B ) \/ x e. ( A Proj C ) ) <-> ( { x } e. ( B " { A } ) \/ { x } e. ( C " { A } ) ) )
6		elun	|- ( x e. ( ( A Proj B ) u. ( A Proj C ) ) <-> ( x e. ( A Proj B ) \/ x e. ( A Proj C ) ) )
7		df-bj-proj	|- ( A Proj ( B u. C ) ) = { x | { x } e. ( ( B u. C ) " { A } ) }
8	7	abeq2i	|- ( x e. ( A Proj ( B u. C ) ) <-> { x } e. ( ( B u. C ) " { A } ) )
9		imaundir	|- ( ( B u. C ) " { A } ) = ( ( B " { A } ) u. ( C " { A } ) )
10	9	eleq2i	|- ( { x } e. ( ( B u. C ) " { A } ) <-> { x } e. ( ( B " { A } ) u. ( C " { A } ) ) )
11		elun	|- ( { x } e. ( ( B " { A } ) u. ( C " { A } ) ) <-> ( { x } e. ( B " { A } ) \/ { x } e. ( C " { A } ) ) )
12	8 10 11	3bitri	|- ( x e. ( A Proj ( B u. C ) ) <-> ( { x } e. ( B " { A } ) \/ { x } e. ( C " { A } ) ) )
13	5 6 12	3bitr4ri	|- ( x e. ( A Proj ( B u. C ) ) <-> x e. ( ( A Proj B ) u. ( A Proj C ) ) )
14	13	eqriv	|- ( A Proj ( B u. C ) ) = ( ( A Proj B ) u. ( A Proj C ) )