Theorem imaco 6198

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 3057	. . 3 ⊢ (∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥))
2		vex 3440	. . . 4 ⊢ 𝑥 ∈ V
3	2	elima 6014	. . 3 ⊢ (𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)) ↔ ∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥)
4		vex 3440	. . . . . . 7 ⊢ 𝑧 ∈ V
5	4, 2	brco 5810	. . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
6	5	rexbii 3079	. . . . 5 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
7		rexcom4 3259	. . . . 5 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
8		r19.41v 3162	. . . . . 6 ⊢ (∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
9	8	exbii 1849	. . . . 5 ⊢ (∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
10	6, 7, 9	3bitri 297	. . . 4 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
11	2	elima 6014	. . . 4 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥)
12		vex 3440	. . . . . . 7 ⊢ 𝑦 ∈ V
13	12	elima 6014	. . . . . 6 ⊢ (𝑦 ∈ (𝐵 “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧𝐵𝑦)
14	13	anbi1i 624	. . . . 5 ⊢ ((𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
15	14	exbii 1849	. . . 4 ⊢ (∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
16	10, 11, 15	3bitr4i 303	. . 3 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥))
17	1, 3, 16	3bitr4ri 304	. 2 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)))
18	17	eqriv 2728	1 ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056   class class class wbr 5091   “ cima 5619   ∘ ccom 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-11 2160  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-xp 5622  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629

This theorem is referenced by:  fvco2  6919  suppco  8136  fipreima  9242  fsuppcolem  9285  psgnunilem1  19403  gsumzf1o  19822  dprdf1o  19944  frlmup3  21735  f1lindf  21757  lindfmm  21762  cnco  23179  cnpco  23180  ptrescn  23552  xkoco1cn  23570  xkoco2cn  23571  xkococnlem  23572  qtopcn  23627  fmco  23874  uniioombllem3  25511  cncombf  25584  deg1val  26026  ofpreima  32642  esplysply  33587  mbfmco  34272  eulerpartlemmf  34383  erdsze2lem2  35236  cvmliftmolem1  35313  cvmlift2lem9a  35335  cvmlift2lem9  35343  mclsppslem  35615  bj-imdirco  37223  poimirlem15  37674  poimirlem16  37675  poimirlem19  37678  cnambfre  37707  ftc1anclem3  37734  aks6d1c6lem4  42205  aks6d1c6lem5  42209  trclimalb2  43758  brtrclfv2  43759  frege97d  43784  frege109d  43789  frege131d  43796  extoimad  44196  imo72b2lem0  44197  imo72b2lem2  44199  imo72b2lem1  44201  imo72b2  44204  limccog  45659  smfco  46839  afv2co2  47287  grimco  47919