Theorem reluni

Description: The union of a class is a relation iff any member is a relation. Exercise 6 of TakeutiZaring p. 25 and its converse. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	reluni	$$⊢\mathrm{Rel}\bigcup A\leftrightarrow \forall x\in A\mathrm{Rel}x$$

Proof

Step	Hyp	Ref	Expression
1		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
2	1	releqi	$$⊢\mathrm{Rel}\bigcup A\leftrightarrow \mathrm{Rel}\bigcup _{x\in A}x$$
3		reliun	$$⊢\mathrm{Rel}\bigcup _{x\in A}x\leftrightarrow \forall x\in A\mathrm{Rel}x$$
4	2 3	bitri	$$⊢\mathrm{Rel}\bigcup A\leftrightarrow \forall x\in A\mathrm{Rel}x$$