Theorem imaco 6224

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 3054	. . 3 ⊢ (∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥))
2		vex 3451	. . . 4 ⊢ 𝑥 ∈ V
3	2	elima 6036	. . 3 ⊢ (𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)) ↔ ∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥)
4		vex 3451	. . . . . . 7 ⊢ 𝑧 ∈ V
5	4, 2	brco 5834	. . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
6	5	rexbii 3076	. . . . 5 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
7		rexcom4 3264	. . . . 5 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
8		r19.41v 3167	. . . . . 6 ⊢ (∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
9	8	exbii 1848	. . . . 5 ⊢ (∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
10	6, 7, 9	3bitri 297	. . . 4 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
11	2	elima 6036	. . . 4 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥)
12		vex 3451	. . . . . . 7 ⊢ 𝑦 ∈ V
13	12	elima 6036	. . . . . 6 ⊢ (𝑦 ∈ (𝐵 “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧𝐵𝑦)
14	13	anbi1i 624	. . . . 5 ⊢ ((𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
15	14	exbii 1848	. . . 4 ⊢ (∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))
16	10, 11, 15	3bitr4i 303	. . 3 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥))
17	1, 3, 16	3bitr4ri 304	. 2 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)))
18	17	eqriv 2726	1 ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053   class class class wbr 5107   “ cima 5641   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  fvco2  6958  suppco  8185  fipreima  9309  fsuppcolem  9352  psgnunilem1  19423  gsumzf1o  19842  dprdf1o  19964  frlmup3  21709  f1lindf  21731  lindfmm  21736  cnco  23153  cnpco  23154  ptrescn  23526  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  qtopcn  23601  fmco  23848  uniioombllem3  25486  cncombf  25559  deg1val  26001  ofpreima  32589  mbfmco  34255  eulerpartlemmf  34366  erdsze2lem2  35191  cvmliftmolem1  35268  cvmlift2lem9a  35290  cvmlift2lem9  35298  mclsppslem  35570  bj-imdirco  37178  poimirlem15  37629  poimirlem16  37630  poimirlem19  37633  cnambfre  37662  ftc1anclem3  37689  aks6d1c6lem4  42161  aks6d1c6lem5  42165  trclimalb2  43715  brtrclfv2  43716  frege97d  43741  frege109d  43746  frege131d  43753  extoimad  44153  imo72b2lem0  44154  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  limccog  45618  smfco  46800  afv2co2  47258  grimco  47889