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	|- ( A. x e. A Tr x -> Tr U. A )

Proof

Step	Hyp	Ref	Expression
1		triun	|- ( A. x e. A Tr x -> Tr U_ x e. A x )
2		uniiun	|- U. A = U_ x e. A x
3		treq	|- ( U. A = U_ x e. A x -> ( Tr U. A <-> Tr U_ x e. A x ) )
4	2 3	ax-mp	|- ( Tr U. A <-> Tr U_ x e. A x )
5	1 4	sylibr	|- ( A. x e. A Tr x -> Tr U. A )