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

Metamath Proof Explorer

Theorem trint

Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of Enderton p. 73. (Contributed by Scott Fenton, 25-Feb-2011) (Proof shortened by BJ, 3-Oct-2022)

Ref Expression
Assertion trint ⊢ ∀ x ∈ A Tr ⁡ x → Tr ⁡ ⋂ A

Proof

Step Hyp Ref Expression
1 triin ⊢ ∀ x ∈ A Tr ⁡ x → Tr ⁡ ⋂ x ∈ A x
2 intiin ⊢ ⋂ 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