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	|- ( A. x e. A Tr x -> Tr |^| A )

Proof

Step	Hyp	Ref	Expression
1		triin	|- ( A. x e. A Tr x -> Tr |^|_ x e. A x )
2		intiin	|- |^| A = |^|_ x e. A x
3		treq	|- ( |^| A = |^|_ x e. A x -> ( Tr |^| A <-> Tr |^|_ x e. A x ) )
4	2 3	ax-mp	|- ( Tr |^| A <-> Tr |^|_ x e. A x )
5	1 4	sylibr	|- ( A. x e. A Tr x -> Tr |^| A )