Theorem relun

Description: The union of two relations is a relation. Compare Exercise 5 of TakeutiZaring p. 25. (Contributed by NM, 12-Aug-1994)

	Ref	Expression
Assertion	relun	$$⊢\mathrm{Rel}\left(A\cup B\right)\leftrightarrow \left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		unss	$$⊢\left(A\subseteq \mathrm{V}\times \mathrm{V}\wedge B\subseteq \mathrm{V}\times \mathrm{V}\right)\leftrightarrow A\cup B\subseteq \mathrm{V}\times \mathrm{V}$$
2		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
3		df-rel	$$⊢\mathrm{Rel}B\leftrightarrow B\subseteq \mathrm{V}\times \mathrm{V}$$
4	2 3	anbi12i	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\leftrightarrow \left(A\subseteq \mathrm{V}\times \mathrm{V}\wedge B\subseteq \mathrm{V}\times \mathrm{V}\right)$$
5		df-rel	$$⊢\mathrm{Rel}\left(A\cup B\right)\leftrightarrow A\cup B\subseteq \mathrm{V}\times \mathrm{V}$$
6	1 4 5	3bitr4ri	$$⊢\mathrm{Rel}\left(A\cup B\right)\leftrightarrow \left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)$$