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	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		triun	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝑥 ∈ 𝐴 𝑥 )
2		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
3		treq	⊢ ( ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 → ( Tr ∪ 𝐴 ↔ Tr ∪ 𝑥 ∈ 𝐴 𝑥 ) )
4	2 3	ax-mp	⊢ ( Tr ∪ 𝐴 ↔ Tr ∪ 𝑥 ∈ 𝐴 𝑥 )
5	1 4	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴 )