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 \cup C)) = (A Proj B) \cup (A Proj C)$

Step	Hyp	Ref	Expression
1		df-bj-proj	$⊢ (A Proj B) = \{x \| \{x\} \in B [\{A\}]\}$
2	1	abeq2i	$⊢ x \in (A Proj B) \leftrightarrow \{x\} \in B [\{A\}]$
3		df-bj-proj	$⊢ (A Proj C) = \{x \| \{x\} \in C [\{A\}]\}$
4	3	abeq2i	$⊢ x \in (A Proj C) \leftrightarrow \{x\} \in C [\{A\}]$
5	2 4	orbi12i	$⊢ (x \in (A Proj B) \lor x \in (A Proj C)) \leftrightarrow (\{x\} \in B [\{A\}] \lor \{x\} \in C [\{A\}])$
6		elun	$⊢ x \in ((A Proj B) \cup (A Proj C)) \leftrightarrow (x \in (A Proj B) \lor x \in (A Proj C))$
7		df-bj-proj	$⊢ (A Proj (B \cup C)) = \{x \| \{x\} \in (B \cup C) [\{A\}]\}$
8	7	abeq2i	$⊢ x \in (A Proj (B \cup C)) \leftrightarrow \{x\} \in (B \cup C) [\{A\}]$
9		imaundir	$⊢ (B \cup C) [\{A\}] = B [\{A\}] \cup C [\{A\}]$
10	9	eleq2i	$⊢ \{x\} \in (B \cup C) [\{A\}] \leftrightarrow \{x\} \in (B [\{A\}] \cup C [\{A\}])$
11		elun	$⊢ \{x\} \in (B [\{A\}] \cup C [\{A\}]) \leftrightarrow (\{x\} \in B [\{A\}] \lor \{x\} \in C [\{A\}])$
12	8 10 11	3bitri	$⊢ x \in (A Proj (B \cup C)) \leftrightarrow (\{x\} \in B [\{A\}] \lor \{x\} \in C [\{A\}])$
13	5 6 12	3bitr4ri	$⊢ x \in (A Proj (B \cup C)) \leftrightarrow x \in ((A Proj B) \cup (A Proj C))$
14	13	eqriv	$⊢ (A Proj (B \cup C)) = (A Proj B) \cup (A Proj C)$

Metamath Proof Explorer