Theorem truni

Description: The union of a class of transitive sets is transitive. Exercise 5(a) of Enderton p. 73. (Contributed by Scott Fenton, 21-Feb-2011) (Proof shortened by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Assertion	truni	$$⊢\forall x\in A\mathrm{Tr}x\to \mathrm{Tr}\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		triun	$$⊢\forall x\in A\mathrm{Tr}x\to \mathrm{Tr}\bigcup _{x\in A}x$$
2		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
3		treq	$$⊢\bigcup A=\bigcup _{x\in A}x\to \left(\mathrm{Tr}\bigcup A\leftrightarrow \mathrm{Tr}\bigcup _{x\in A}x\right)$$
4	2 3	ax-mp	$$⊢\mathrm{Tr}\bigcup A\leftrightarrow \mathrm{Tr}\bigcup _{x\in A}x$$
5	1 4	sylibr	$$⊢\forall x\in A\mathrm{Tr}x\to \mathrm{Tr}\bigcup A$$