This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∪ 𝐴 )