Theorem trrelind

Description: The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypotheses	trrelind.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
	trrelind.s	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )
	trrelind.t	⊢ ( 𝜑 → 𝑇 = ( 𝑅 ∩ 𝑆 ) )
Assertion	trrelind	⊢ ( 𝜑 → ( 𝑇 ∘ 𝑇 ) ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		trrelind.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
2		trrelind.s	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )
3		trrelind.t	⊢ ( 𝜑 → 𝑇 = ( 𝑅 ∩ 𝑆 ) )
4		inss1	⊢ ( 𝑅 ∩ 𝑆 ) ⊆ 𝑅
5	4	a1i	⊢ ( 𝜑 → ( 𝑅 ∩ 𝑆 ) ⊆ 𝑅 )
6	1 5 5	trrelssd	⊢ ( 𝜑 → ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) ⊆ 𝑅 )
7		inss2	⊢ ( 𝑅 ∩ 𝑆 ) ⊆ 𝑆
8	7	a1i	⊢ ( 𝜑 → ( 𝑅 ∩ 𝑆 ) ⊆ 𝑆 )
9	2 8 8	trrelssd	⊢ ( 𝜑 → ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) ⊆ 𝑆 )
10	6 9	ssind	⊢ ( 𝜑 → ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) ⊆ ( 𝑅 ∩ 𝑆 ) )
11	3 3	coeq12d	⊢ ( 𝜑 → ( 𝑇 ∘ 𝑇 ) = ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) )
12	10 11 3	3sstr4d	⊢ ( 𝜑 → ( 𝑇 ∘ 𝑇 ) ⊆ 𝑇 )