Theorem imaco 6257

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

Assertion

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

Proof of Theorem imaco

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∃wrex 3092   class class class wbr 5114   “ cima 5669   ∘ ccom 5670

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-11 2195  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is used by:  fvco2  6985  suppco  8211  fipreima  9325  fsuppcolem  9371  psgnunilem1  19594  gsumzf1o  20013  dprdf1o  20135  frlmup3  21987  f1lindf  22009  lindfmm  22014  cnco  23460  cnpco  23461  ptrescn  23833  xkoco1cn  23851  xkoco2cn  23852  xkococnlem  23853  qtopcn  23908  fmco  24155  uniioombllem3  25781  cncombf  25854  deg1val  26290  ofpreima  33047  esplysply  33992  mbfmco  34686  eulerpartlemmf  34797  erdsze2lem2  35717  cvmliftmolem1  35794  cvmlift2lem9a  35816  cvmlift2lem9  35824  mclsppslem  36096  bj-imdirco  37875  poimirlem15  38327  poimirlem16  38328  poimirlem19  38331  cnambfre  38360  ftc1anclem3  38387  aks6d1c6lem4  42981  aks6d1c6lem5  42985  trclimalb2  44493  brtrclfv2  44494  frege97d  44519  frege109d  44524  frege131d  44531  extoimad  44931  imo72b2lem0  44932  imo72b2lem2  44934  imo72b2lem1  44936  imo72b2  44939  limccog  46377  smfco  47557  afv2co2  48035  grimco  48695