Theorem coxp

Description: Composition with a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	coxp	⊢ ( 𝐴 ∘ ( 𝐵 × 𝐶 ) ) = ( 𝐵 × ( 𝐴 “ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( 𝐴 ∘ ( 𝐵 × 𝐶 ) )
2		relxp	⊢ Rel ( 𝐵 × ( 𝐴 “ 𝐶 ) )
3		brxp	⊢ ( 𝑥 ( 𝐵 × 𝐶 ) 𝑧 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
4	3	anbi1i	⊢ ( ( 𝑥 ( 𝐵 × 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑧 𝐴 𝑦 ) )
5		anass	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) )
6	4 5	bitri	⊢ ( ( 𝑥 ( 𝐵 × 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) )
7	6	exbii	⊢ ( ∃ 𝑧 ( 𝑥 ( 𝐵 × 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) )
8		vex	⊢ 𝑥 ∈ V
9		vex	⊢ 𝑦 ∈ V
10	8 9	opelco	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑧 ( 𝑥 ( 𝐵 × 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
11	9	elima2	⊢ ( 𝑦 ∈ ( 𝐴 “ 𝐶 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) )
12	11	anbi2i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐴 “ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) )
13		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × ( 𝐴 “ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐴 “ 𝐶 ) ) )
14		19.42v	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) )
15	12 13 14	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × ( 𝐴 “ 𝐶 ) ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑧 𝐴 𝑦 ) ) )
16	7 10 15	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ( 𝐵 × 𝐶 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × ( 𝐴 “ 𝐶 ) ) )
17	1 2 16	eqrelriiv	⊢ ( 𝐴 ∘ ( 𝐵 × 𝐶 ) ) = ( 𝐵 × ( 𝐴 “ 𝐶 ) )