![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imaco | Structured version Visualization version GIF version |
Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) |
Ref | Expression |
---|---|
imaco | ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 3095 | . . 3 ⊢ (∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥)) | |
2 | vex 3419 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | elima 5775 | . . 3 ⊢ (𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)) ↔ ∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥) |
4 | rexcom4 3197 | . . . . 5 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) | |
5 | r19.41v 3289 | . . . . . 6 ⊢ (∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) | |
6 | 5 | exbii 1810 | . . . . 5 ⊢ (∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
7 | 4, 6 | bitri 267 | . . . 4 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
8 | 2 | elima 5775 | . . . . 5 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥) |
9 | vex 3419 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
10 | 9, 2 | brco 5591 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
11 | 10 | rexbii 3195 | . . . . 5 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
12 | 8, 11 | bitri 267 | . . . 4 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
13 | vex 3419 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
14 | 13 | elima 5775 | . . . . . 6 ⊢ (𝑦 ∈ (𝐵 “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧𝐵𝑦) |
15 | 14 | anbi1i 614 | . . . . 5 ⊢ ((𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
16 | 15 | exbii 1810 | . . . 4 ⊢ (∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
17 | 7, 12, 16 | 3bitr4i 295 | . . 3 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥)) |
18 | 1, 3, 17 | 3bitr4ri 296 | . 2 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶))) |
19 | 18 | eqriv 2776 | 1 ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 = wceq 1507 ∃wex 1742 ∈ wcel 2050 ∃wrex 3090 class class class wbr 4929 “ cima 5410 ∘ ccom 5411 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-xp 5413 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 |
This theorem is referenced by: fvco2 6586 suppco 7673 supp0cosupp0OLD 7676 imacosuppOLD 7678 fipreima 8625 fsuppcolem 8659 psgnunilem1 18382 gsumzf1o 18786 dprdf1o 18904 frlmup3 20646 f1lindf 20668 lindfmm 20673 cnco 21578 cnpco 21579 ptrescn 21951 xkoco1cn 21969 xkoco2cn 21970 xkococnlem 21971 qtopcn 22026 fmco 22273 uniioombllem3 23889 cncombf 23962 deg1val 24393 ofpreima 30172 mbfmco 31164 eulerpartlemmf 31275 erdsze2lem2 32033 cvmliftmolem1 32110 cvmlift2lem9a 32132 cvmlift2lem9 32140 mclsppslem 32347 poimirlem15 34345 poimirlem16 34346 poimirlem19 34349 cnambfre 34378 ftc1anclem3 34407 trclimalb2 39431 brtrclfv2 39432 frege97d 39457 frege109d 39462 frege131d 39469 extoimad 39876 imo72b2lem0 39877 imo72b2lem2 39879 imo72b2lem1 39883 imo72b2 39887 limccog 41330 smfco 42506 afv2co2 42860 isomgrtrlem 43369 |
Copyright terms: Public domain | W3C validator |