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

Proof

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