Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funco | Structured version Visualization version GIF version |
Description: The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
funco | ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funmo 6405 | . . . . 5 ⊢ (Fun 𝐺 → ∃*𝑧 𝑥𝐺𝑧) | |
2 | funmo 6405 | . . . . . 6 ⊢ (Fun 𝐹 → ∃*𝑦 𝑧𝐹𝑦) | |
3 | 2 | alrimiv 1935 | . . . . 5 ⊢ (Fun 𝐹 → ∀𝑧∃*𝑦 𝑧𝐹𝑦) |
4 | moexexvw 2630 | . . . . 5 ⊢ ((∃*𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) | |
5 | 1, 3, 4 | syl2anr 600 | . . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) |
6 | 5 | alrimiv 1935 | . . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) |
7 | funopab 6424 | . . 3 ⊢ (Fun {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)} ↔ ∀𝑥∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) | |
8 | 6, 7 | sylibr 237 | . 2 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)}) |
9 | df-co 5569 | . . 3 ⊢ (𝐹 ∘ 𝐺) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)} | |
10 | 9 | funeqi 6410 | . 2 ⊢ (Fun (𝐹 ∘ 𝐺) ↔ Fun {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)}) |
11 | 8, 10 | sylibr 237 | 1 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wal 1541 ∃wex 1787 ∃*wmo 2538 class class class wbr 5062 {copab 5124 ∘ ccom 5564 Fun wfun 6383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5201 ax-nul 5208 ax-pr 5331 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3417 df-dif 3878 df-un 3880 df-in 3882 df-ss 3892 df-nul 4247 df-if 4449 df-sn 4551 df-pr 4553 df-op 4557 df-br 5063 df-opab 5125 df-id 5464 df-xp 5566 df-rel 5567 df-cnv 5568 df-co 5569 df-fun 6391 |
This theorem is referenced by: funresfunco 6430 fncofn 6502 fncoOLD 6504 fco3OLD 6588 f1cof1 6635 f1coOLD 6637 curry1 7881 curry2 7884 tposfun 7993 fsuppco 9031 fsuppco2 9032 fsuppcor 9033 fin23lem30 9969 smobeth 10213 hashkf 13911 xppreima 30715 smatrcl 31473 comptiunov2i 41006 hoicvr 43776 |
Copyright terms: Public domain | W3C validator |