Theorem funco 6557

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.)

Assertion

Ref	Expression
funco	⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))

Proof of Theorem funco

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funmo 6533	. . . . 5 ⊢ (Fun 𝐺 → ∃*𝑧 𝑥𝐺𝑧)
2		funmo 6533	. . . . . 6 ⊢ (Fun 𝐹 → ∃*𝑦 𝑧𝐹𝑦)
3	2	alrimiv 1946	. . . . 5 ⊢ (Fun 𝐹 → ∀𝑧∃*𝑦 𝑧𝐹𝑦)
4		moexexvw 2654	. . . . 5 ⊢ ((∃*𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
5	1, 3, 4	syl2anr 606	. . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
6	5	alrimiv 1946	. . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
7		funopab 6552	. . 3 ⊢ (Fun {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)} ↔ ∀𝑥∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
8	6, 7	sylibr 236	. 2 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)})
9		df-co 5654	. . 3 ⊢ (𝐹 ∘ 𝐺) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)}
10	9	funeqi 6538	. 2 ⊢ (Fun (𝐹 ∘ 𝐺) ↔ Fun {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)})
11	8, 10	sylibr 236	1 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1557  ∃wex 1798  ∃*wmo 2563   class class class wbr 5099  {copab 5161   ∘ ccom 5649  Fun wfun 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-fun 6519

This theorem is referenced by:  funresfunco  6558  fncofn  6634  f1cof1  6768  curry1  8078  curry2  8081  tposfun  8217  fsuppco  9345  fsuppco2  9346  fsuppcor  9347  fin23lem30  10296  smobeth  10541  hashkf  14342  precsexlem10  28286  precsexlem11  28287  xppreima  32797  smatrcl  34054  comptiunov2i  44246  hoicvr  47086  upgrimpthslem1  48493  upgrimspths  48496