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	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍 ) ∧ ( 𝐴 𝐷 𝑋 ∧ 𝑋 𝐶 𝐵 ) ) → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )