![]() |
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 3072 | . . 3 ⊢ (∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥)) | |
2 | vex 3479 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | elima 6065 | . . 3 ⊢ (𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶)) ↔ ∃𝑦 ∈ (𝐵 “ 𝐶)𝑦𝐴𝑥) |
4 | rexcom4 3286 | . . . . 5 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) | |
5 | r19.41v 3189 | . . . . . 6 ⊢ (∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) | |
6 | 5 | exbii 1851 | . . . . 5 ⊢ (∃𝑦∃𝑧 ∈ 𝐶 (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
7 | 4, 6 | bitri 275 | . . . 4 ⊢ (∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
8 | 2 | elima 6065 | . . . . 5 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥) |
9 | vex 3479 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
10 | 9, 2 | brco 5871 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
11 | 10 | rexbii 3095 | . . . . 5 ⊢ (∃𝑧 ∈ 𝐶 𝑧(𝐴 ∘ 𝐵)𝑥 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
12 | 8, 11 | bitri 275 | . . . 4 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
13 | vex 3479 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
14 | 13 | elima 6065 | . . . . . 6 ⊢ (𝑦 ∈ (𝐵 “ 𝐶) ↔ ∃𝑧 ∈ 𝐶 𝑧𝐵𝑦) |
15 | 14 | anbi1i 625 | . . . . 5 ⊢ ((𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
16 | 15 | exbii 1851 | . . . 4 ⊢ (∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧 ∈ 𝐶 𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)) |
17 | 7, 12, 16 | 3bitr4i 303 | . . 3 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵 “ 𝐶) ∧ 𝑦𝐴𝑥)) |
18 | 1, 3, 17 | 3bitr4ri 304 | . 2 ⊢ (𝑥 ∈ ((𝐴 ∘ 𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵 “ 𝐶))) |
19 | 18 | eqriv 2730 | 1 ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∃wrex 3071 class class class wbr 5149 “ cima 5680 ∘ ccom 5681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-11 2155 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-xp 5683 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 |
This theorem is referenced by: fvco2 6989 suppco 8191 fipreima 9358 fsuppcolem 9396 psgnunilem1 19361 gsumzf1o 19780 dprdf1o 19902 frlmup3 21355 f1lindf 21377 lindfmm 21382 cnco 22770 cnpco 22771 ptrescn 23143 xkoco1cn 23161 xkoco2cn 23162 xkococnlem 23163 qtopcn 23218 fmco 23465 uniioombllem3 25102 cncombf 25175 deg1val 25614 ofpreima 31890 mbfmco 33263 eulerpartlemmf 33374 erdsze2lem2 34195 cvmliftmolem1 34272 cvmlift2lem9a 34294 cvmlift2lem9 34302 mclsppslem 34574 bj-imdirco 36071 poimirlem15 36503 poimirlem16 36504 poimirlem19 36507 cnambfre 36536 ftc1anclem3 36563 trclimalb2 42477 brtrclfv2 42478 frege97d 42503 frege109d 42508 frege131d 42515 extoimad 42916 imo72b2lem0 42917 imo72b2lem2 42919 imo72b2lem1 42921 imo72b2 42924 limccog 44336 smfco 45518 afv2co2 45965 isomgrtrlem 46506 |
Copyright terms: Public domain | W3C validator |