![]() |
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 3070 | . . 3 ⊢ (∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥)) | |
2 | vex 3477 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | elima 6064 | . . 3 ⊢ (𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)) ↔ ∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥) |
4 | rexcom4 3284 | . . . . 5 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) | |
5 | r19.41v 3187 | . . . . . 6 ⊢ (∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) | |
6 | 5 | exbii 1849 | . . . . 5 ⊢ (∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
7 | 4, 6 | bitri 275 | . . . 4 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
8 | 2 | elima 6064 | . . . . 5 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥) |
9 | vex 3477 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
10 | 9, 2 | brco 5870 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
11 | 10 | rexbii 3093 | . . . . 5 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
12 | 8, 11 | bitri 275 | . . . 4 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
13 | vex 3477 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
14 | 13 | elima 6064 | . . . . . 6 ⊢ (𝑦 ∈ (𝐵 “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧𝐵𝑦) |
15 | 14 | anbi1i 623 | . . . . 5 ⊢ ((𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
16 | 15 | exbii 1849 | . . . 4 ⊢ (∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
17 | 7, 12, 16 | 3bitr4i 303 | . . 3 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥)) |
18 | 1, 3, 17 | 3bitr4ri 304 | . 2 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶))) |
19 | 18 | eqriv 2728 | 1 ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ∃wrex 3069 class class class wbr 5148 “ cima 5679 ∘ ccom 5680 |
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 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-11 2153 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 |
This theorem is referenced by: fvco2 6988 suppco 8197 fipreima 9364 fsuppcolem 9402 psgnunilem1 19409 gsumzf1o 19828 dprdf1o 19950 frlmup3 21665 f1lindf 21687 lindfmm 21692 cnco 23090 cnpco 23091 ptrescn 23463 xkoco1cn 23481 xkoco2cn 23482 xkococnlem 23483 qtopcn 23538 fmco 23785 uniioombllem3 25434 cncombf 25507 deg1val 25952 ofpreima 32323 mbfmco 33727 eulerpartlemmf 33838 erdsze2lem2 34659 cvmliftmolem1 34736 cvmlift2lem9a 34758 cvmlift2lem9 34766 mclsppslem 35038 bj-imdirco 36535 poimirlem15 36967 poimirlem16 36968 poimirlem19 36971 cnambfre 37000 ftc1anclem3 37027 trclimalb2 42940 brtrclfv2 42941 frege97d 42966 frege109d 42971 frege131d 42978 extoimad 43379 imo72b2lem0 43380 imo72b2lem2 43382 imo72b2lem1 43384 imo72b2 43387 limccog 44795 smfco 45977 afv2co2 46424 isomgrtrlem 46965 |
Copyright terms: Public domain | W3C validator |