This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brcogw

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

Ref Expression
Assertion brcogw ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍 ) ∧ ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) ) → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )

Proof

Step Hyp Ref Expression
1 3simpa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
2 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐴 𝐷 𝑥 ↔ 𝐴 𝐷 𝑋 ) )
3 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐶 𝐵 ↔ 𝑋 𝐶 𝐵 ) )
4 2 3 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ↔ ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) ) )
5 4 spcegv ⊢ ( 𝑋 ∈ 𝑍 → ( ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) → ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )
6 5 imp ⊢ ( ( 𝑋 ∈ 𝑍 ∧ ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) ) → ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) )
7 6 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍 ) ∧ ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) ) → ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) )
8 brcog ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )
9 8 biimpar ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )
10 1 7 9 syl2an2r ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍 ) ∧ ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) ) → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )