Metamath Proof Explorer

Theorem brcogw

Description: Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018)

Ref Expression
Assertion brcogw ⊢ A ∈ V ∧ B ∈ W ∧ X ∈ Z ∧ A D X ∧ X C B → A C ∘ D B

Proof

Step Hyp Ref Expression
1 3simpa ⊢ A ∈ V ∧ B ∈ W ∧ X ∈ Z → A ∈ V ∧ B ∈ W
2 breq2 ⊢ x = X → A D x ↔ A D X
3 breq1 ⊢ x = X → x C B ↔ X C B
4 2 3 anbi12d ⊢ x = X → A D x ∧ x C B ↔ A D X ∧ X C B
5 4 spcegv ⊢ X ∈ Z → A D X ∧ X C B → ∃ x A D x ∧ x C B
6 5 imp ⊢ X ∈ Z ∧ A D X ∧ X C B → ∃ x A D x ∧ x C B
7 6 3ad2antl3 ⊢ A ∈ V ∧ B ∈ W ∧ X ∈ Z ∧ A D X ∧ X C B → ∃ x A D x ∧ x C B
8 brcog ⊢ A ∈ V ∧ B ∈ W → A C ∘ D B ↔ ∃ x A D x ∧ x C B
9 8 biimpar ⊢ A ∈ V ∧ B ∈ W ∧ ∃ x A D x ∧ x C B → A C ∘ D B
10 1 7 9 syl2an2r ⊢ A ∈ V ∧ B ∈ W ∧ X ∈ Z ∧ A D X ∧ X C B → A C ∘ D B