Theorem brcoi

Description: Ordered pair membership in a composition. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Hypotheses	brcoi.1	⊢ 𝑋 ∈ V
	brcoi.2	⊢ 𝑌 ∈ V
	brcoi.3	⊢ 𝑍 ∈ V
Assertion	brcoi	⊢ ( ( 𝑋 𝑅 𝑌 ∧ 𝑌 𝑆 𝑍 ) → 𝑋 ( 𝑆 ∘ 𝑅 ) 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		brcoi.1	⊢ 𝑋 ∈ V
2		brcoi.2	⊢ 𝑌 ∈ V
3		brcoi.3	⊢ 𝑍 ∈ V
4	1 3 2	3pm3.2i	⊢ ( 𝑋 ∈ V ∧ 𝑍 ∈ V ∧ 𝑌 ∈ V )
5		brcogw	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑍 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑋 𝑅 𝑌 ∧ 𝑌 𝑆 𝑍 ) ) → 𝑋 ( 𝑆 ∘ 𝑅 ) 𝑍 )
6	4 5	mpan	⊢ ( ( 𝑋 𝑅 𝑌 ∧ 𝑌 𝑆 𝑍 ) → 𝑋 ( 𝑆 ∘ 𝑅 ) 𝑍 )