rnun

Description: Distributive law for range over union. Theorem 8 of Suppes p. 60. (Contributed by NM, 24-Mar-1998)

		Ref	Expression
	Assertion	rnun	$⊢ ran (A \cup B) = ran A \cup ran B$

Step	Hyp	Ref	Expression
1		cnvun	$⊢ {(A \cup B)}^{-1} = A^{-1} \cup B^{-1}$
2	1	dmeqi	$⊢ dom {(A \cup B)}^{-1} = dom (A^{-1} \cup B^{-1})$
3		dmun	$⊢ dom (A^{-1} \cup B^{-1}) = dom A^{-1} \cup dom B^{-1}$
4	2 3	eqtri	$⊢ dom {(A \cup B)}^{-1} = dom A^{-1} \cup dom B^{-1}$
5		df-rn	$⊢ ran (A \cup B) = dom {(A \cup B)}^{-1}$
6		df-rn	$⊢ ran A = dom A^{-1}$
7		df-rn	$⊢ ran B = dom B^{-1}$
8	6 7	uneq12i	$⊢ ran A \cup ran B = dom A^{-1} \cup dom B^{-1}$
9	4 5 8	3eqtr4i	$⊢ ran (A \cup B) = ran A \cup ran B$

Metamath Proof Explorer