![]() |
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 6201 | . . . . 5 ⊢ (Fun 𝐺 → ∃*𝑧 𝑥𝐺𝑧) | |
2 | funmo 6201 | . . . . . 6 ⊢ (Fun 𝐹 → ∃*𝑦 𝑧𝐹𝑦) | |
3 | 2 | alrimiv 1886 | . . . . 5 ⊢ (Fun 𝐹 → ∀𝑧∃*𝑦 𝑧𝐹𝑦) |
4 | moexexv 2671 | . . . . 5 ⊢ ((∃*𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) | |
5 | 1, 3, 4 | syl2anr 587 | . . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) |
6 | 5 | alrimiv 1886 | . . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) |
7 | funopab 6220 | . . 3 ⊢ (Fun {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)} ↔ ∀𝑥∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)) | |
8 | 6, 7 | sylibr 226 | . 2 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)}) |
9 | df-co 5412 | . . 3 ⊢ (𝐹 ∘ 𝐺) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)} | |
10 | 9 | funeqi 6206 | . 2 ⊢ (Fun (𝐹 ∘ 𝐺) ↔ Fun {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)}) |
11 | 8, 10 | sylibr 226 | 1 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∀wal 1505 ∃wex 1742 ∃*wmo 2545 class class class wbr 4925 {copab 4987 ∘ ccom 5407 Fun wfun 6179 |
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 2744 ax-sep 5056 ax-nul 5063 ax-pr 5182 |
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 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4926 df-opab 4988 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-fun 6187 |
This theorem is referenced by: funresfunco 6226 fnco 6295 f1co 6411 curry1 7605 curry2 7608 tposfun 7709 fsuppco 8658 fsuppco2 8659 fsuppcor 8660 fin23lem30 9560 smobeth 9804 hashkf 13505 xppreima 30170 smatrcl 30732 comptiunov2i 39443 fco3 40942 hoicvr 42286 |
Copyright terms: Public domain | W3C validator |