Metamath Proof Explorer

Theorem brcoi

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

Ref Expression
Hypotheses brcoi.1 ⊢ X ∈ V
brcoi.2 ⊢ Y ∈ V
brcoi.3 ⊢ Z ∈ V
Assertion brcoi ⊢ X R Y ∧ Y S Z → X S ∘ R Z

Proof

Step Hyp Ref Expression
1 brcoi.1 ⊢ X ∈ V
2 brcoi.2 ⊢ Y ∈ V
3 brcoi.3 ⊢ Z ∈ V
4 1 3 2 3pm3.2i ⊢ X ∈ V ∧ Z ∈ V ∧ Y ∈ V
5 brcogw ⊢ X ∈ V ∧ Z ∈ V ∧ Y ∈ V ∧ X R Y ∧ Y S Z → X S ∘ R Z
6 4 5 mpan ⊢ X R Y ∧ Y S Z → X S ∘ R Z