Theorem trin

Description: The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994)

	Ref	Expression
Assertion	trin	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → Tr ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
2		trss	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
3		trss	⊢ ( Tr 𝐵 → ( 𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝐵 ) )
4	2 3	im2anan9	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
5	1 4	biimtrid	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
6		ssin	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
7	5 6	imbitrdi	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
8	7	ralrimiv	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
9		dftr3	⊢ ( Tr ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
10	8 9	sylibr	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → Tr ( 𝐴 ∩ 𝐵 ) )