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	$$⊢\forall x\in A\mathrm{Tr}x\to \mathrm{Tr}\bigcap A$$

Proof

Step	Hyp	Ref	Expression
1		triin	$$⊢\forall x\in A\mathrm{Tr}x\to \mathrm{Tr}\bigcap _{x\in A}x$$
2		intiin	$$⊢\bigcap A=\bigcap _{x\in A}x$$
3		treq	$$⊢\bigcap A=\bigcap _{x\in A}x\to \left(\mathrm{Tr}\bigcap A\leftrightarrow \mathrm{Tr}\bigcap _{x\in A}x\right)$$
4	2 3	ax-mp	$$⊢\mathrm{Tr}\bigcap A\leftrightarrow \mathrm{Tr}\bigcap _{x\in A}x$$
5	1 4	sylibr	$$⊢\forall x\in A\mathrm{Tr}x\to \mathrm{Tr}\bigcap A$$