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 ⊢ ∀ x ∈ A Tr ⁡ x → Tr ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 triun ⊢ ∀ x ∈ A Tr ⁡ x → Tr ⁡ ⋃ x ∈ A x
2 uniiun ⊢ ⋃ A = ⋃ x ∈ A x
3 treq ⊢ ⋃ A = ⋃ x ∈ A x → Tr ⁡ ⋃ A ↔ Tr ⁡ ⋃ x ∈ A x
4 2 3 ax-mp ⊢ Tr ⁡ ⋃ A ↔ Tr ⁡ ⋃ x ∈ A x
5 1 4 sylibr ⊢ ∀ x ∈ A Tr ⁡ x → Tr ⁡ ⋃ A