Theorem imaco

Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006)

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

Proof

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