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