Theorem bj-projun

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

	Ref	Expression
Assertion	bj-projun	⊢ ( 𝐴 Proj ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 Proj 𝐵 ) ∪ ( 𝐴 Proj 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-proj	⊢ ( 𝐴 Proj 𝐵 ) = { 𝑥 ∣ { 𝑥 } ∈ ( 𝐵 “ { 𝐴 } ) }
2	1	abeq2i	⊢ ( 𝑥 ∈ ( 𝐴 Proj 𝐵 ) ↔ { 𝑥 } ∈ ( 𝐵 “ { 𝐴 } ) )
3		df-bj-proj	⊢ ( 𝐴 Proj 𝐶 ) = { 𝑥 ∣ { 𝑥 } ∈ ( 𝐶 “ { 𝐴 } ) }
4	3	abeq2i	⊢ ( 𝑥 ∈ ( 𝐴 Proj 𝐶 ) ↔ { 𝑥 } ∈ ( 𝐶 “ { 𝐴 } ) )
5	2 4	orbi12i	⊢ ( ( 𝑥 ∈ ( 𝐴 Proj 𝐵 ) ∨ 𝑥 ∈ ( 𝐴 Proj 𝐶 ) ) ↔ ( { 𝑥 } ∈ ( 𝐵 “ { 𝐴 } ) ∨ { 𝑥 } ∈ ( 𝐶 “ { 𝐴 } ) ) )
6		elun	⊢ ( 𝑥 ∈ ( ( 𝐴 Proj 𝐵 ) ∪ ( 𝐴 Proj 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 Proj 𝐵 ) ∨ 𝑥 ∈ ( 𝐴 Proj 𝐶 ) ) )
7		df-bj-proj	⊢ ( 𝐴 Proj ( 𝐵 ∪ 𝐶 ) ) = { 𝑥 ∣ { 𝑥 } ∈ ( ( 𝐵 ∪ 𝐶 ) “ { 𝐴 } ) }
8	7	abeq2i	⊢ ( 𝑥 ∈ ( 𝐴 Proj ( 𝐵 ∪ 𝐶 ) ) ↔ { 𝑥 } ∈ ( ( 𝐵 ∪ 𝐶 ) “ { 𝐴 } ) )
9		imaundir	⊢ ( ( 𝐵 ∪ 𝐶 ) “ { 𝐴 } ) = ( ( 𝐵 “ { 𝐴 } ) ∪ ( 𝐶 “ { 𝐴 } ) )
10	9	eleq2i	⊢ ( { 𝑥 } ∈ ( ( 𝐵 ∪ 𝐶 ) “ { 𝐴 } ) ↔ { 𝑥 } ∈ ( ( 𝐵 “ { 𝐴 } ) ∪ ( 𝐶 “ { 𝐴 } ) ) )
11		elun	⊢ ( { 𝑥 } ∈ ( ( 𝐵 “ { 𝐴 } ) ∪ ( 𝐶 “ { 𝐴 } ) ) ↔ ( { 𝑥 } ∈ ( 𝐵 “ { 𝐴 } ) ∨ { 𝑥 } ∈ ( 𝐶 “ { 𝐴 } ) ) )
12	8 10 11	3bitri	⊢ ( 𝑥 ∈ ( 𝐴 Proj ( 𝐵 ∪ 𝐶 ) ) ↔ ( { 𝑥 } ∈ ( 𝐵 “ { 𝐴 } ) ∨ { 𝑥 } ∈ ( 𝐶 “ { 𝐴 } ) ) )
13	5 6 12	3bitr4ri	⊢ ( 𝑥 ∈ ( 𝐴 Proj ( 𝐵 ∪ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 Proj 𝐵 ) ∪ ( 𝐴 Proj 𝐶 ) ) )
14	13	eqriv	⊢ ( 𝐴 Proj ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 Proj 𝐵 ) ∪ ( 𝐴 Proj 𝐶 ) )