predun

Description: Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011)

		Ref	Expression
	Assertion	predun	$⊢ Pred (R, (A \cup B), X) = Pred (R, A, X) \cup Pred (R, B, X)$

Step	Hyp	Ref	Expression
1		indir	$⊢ (A \cup B) \cap R^{-1} [\{X\}] = (A \cap R^{-1} [\{X\}]) \cup (B \cap R^{-1} [\{X\}])$
2		df-pred	$⊢ Pred (R, (A \cup B), X) = (A \cup B) \cap R^{-1} [\{X\}]$
3		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
4		df-pred	$⊢ Pred (R, B, X) = B \cap R^{-1} [\{X\}]$
5	3 4	uneq12i	$⊢ Pred (R, A, X) \cup Pred (R, B, X) = (A \cap R^{-1} [\{X\}]) \cup (B \cap R^{-1} [\{X\}])$
6	1 2 5	3eqtr4i	$⊢ Pred (R, (A \cup B), X) = Pred (R, A, X) \cup Pred (R, B, X)$

Metamath Proof Explorer