Theorem imaco

Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006) (Proof shortened by Wolf Lammen, 16-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑦 ∈ ( 𝐵 “ 𝐶 ) 𝑦 𝐴 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝐵 “ 𝐶 ) ∧ 𝑦 𝐴 𝑥 ) )
2		vex	⊢ 𝑥 ∈ V
3	2	elima	⊢ ( 𝑥 ∈ ( 𝐴 “ ( 𝐵 “ 𝐶 ) ) ↔ ∃ 𝑦 ∈ ( 𝐵 “ 𝐶 ) 𝑦 𝐴 𝑥 )
4		vex	⊢ 𝑧 ∈ V
5	4 2	brco	⊢ ( 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑥 ↔ ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
6	5	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐶 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑥 ↔ ∃ 𝑧 ∈ 𝐶 ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
7		rexcom4	⊢ ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
8		r19.41v	⊢ ( ∃ 𝑧 ∈ 𝐶 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
9	8	exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦 ( ∃ 𝑧 ∈ 𝐶 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
10	6 7 9	3bitri	⊢ ( ∃ 𝑧 ∈ 𝐶 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑥 ↔ ∃ 𝑦 ( ∃ 𝑧 ∈ 𝐶 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
11	2	elima	⊢ ( 𝑥 ∈ ( ( 𝐴 ∘ 𝐵 ) “ 𝐶 ) ↔ ∃ 𝑧 ∈ 𝐶 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑥 )
12		vex	⊢ 𝑦 ∈ V
13	12	elima	⊢ ( 𝑦 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑧 ∈ 𝐶 𝑧 𝐵 𝑦 )
14	13	anbi1i	⊢ ( ( 𝑦 ∈ ( 𝐵 “ 𝐶 ) ∧ 𝑦 𝐴 𝑥 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
15	14	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ ( 𝐵 “ 𝐶 ) ∧ 𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦 ( ∃ 𝑧 ∈ 𝐶 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) )
16	10 11 15	3bitr4i	⊢ ( 𝑥 ∈ ( ( 𝐴 ∘ 𝐵 ) “ 𝐶 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝐵 “ 𝐶 ) ∧ 𝑦 𝐴 𝑥 ) )
17	1 3 16	3bitr4ri	⊢ ( 𝑥 ∈ ( ( 𝐴 ∘ 𝐵 ) “ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 “ ( 𝐵 “ 𝐶 ) ) )
18	17	eqriv	⊢ ( ( 𝐴 ∘ 𝐵 ) “ 𝐶 ) = ( 𝐴 “ ( 𝐵 “ 𝐶 ) )