Theorem funco 4960

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		dmcoss 4619	. . . . 5 ⊢ dom (𝐹 ∘ 𝐺) ⊆ dom 𝐺
2		funmo 4937	. . . . . . . . . 10 ⊢ (Fun 𝐹 → ∃*𝑦 𝑧𝐹𝑦)
3	2	alrimiv 1795	. . . . . . . . 9 ⊢ (Fun 𝐹 → ∀𝑧∃*𝑦 𝑧𝐹𝑦)
4	3	ralrimivw 2435	. . . . . . . 8 ⊢ (Fun 𝐹 → ∀𝑥 ∈ dom 𝐺∀𝑧∃*𝑦 𝑧𝐹𝑦)
5		dffun8 4949	. . . . . . . . 9 ⊢ (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥 ∈ dom 𝐺∃!𝑧 𝑥𝐺𝑧))
6	5	simprbi 269	. . . . . . . 8 ⊢ (Fun 𝐺 → ∀𝑥 ∈ dom 𝐺∃!𝑧 𝑥𝐺𝑧)
7	4, 6	anim12ci 332	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (∀𝑥 ∈ dom 𝐺∃!𝑧 𝑥𝐺𝑧 ∧ ∀𝑥 ∈ dom 𝐺∀𝑧∃*𝑦 𝑧𝐹𝑦))
8		r19.26 2485	. . . . . . 7 ⊢ (∀𝑥 ∈ dom 𝐺(∃!𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦) ↔ (∀𝑥 ∈ dom 𝐺∃!𝑧 𝑥𝐺𝑧 ∧ ∀𝑥 ∈ dom 𝐺∀𝑧∃*𝑦 𝑧𝐹𝑦))
9	7, 8	sylibr 132	. . . . . 6 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥 ∈ dom 𝐺(∃!𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦))
10		nfv 1461	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥𝐺𝑧
11	10	euexex 2026	. . . . . . 7 ⊢ ((∃!𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦) → ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
12	11	ralimi 2426	. . . . . 6 ⊢ (∀𝑥 ∈ dom 𝐺(∃!𝑧 𝑥𝐺𝑧 ∧ ∀𝑧∃*𝑦 𝑧𝐹𝑦) → ∀𝑥 ∈ dom 𝐺∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
13	9, 12	syl 14	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥 ∈ dom 𝐺∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
14		ssralv 3058	. . . . 5 ⊢ (dom (𝐹 ∘ 𝐺) ⊆ dom 𝐺 → (∀𝑥 ∈ dom 𝐺∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦) → ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)))
15	1, 13, 14	mpsyl 64	. . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
16		df-br 3786	. . . . . . 7 ⊢ (𝑥(𝐹 ∘ 𝐺)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐹 ∘ 𝐺))
17		df-co 4372	. . . . . . . 8 ⊢ (𝐹 ∘ 𝐺) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)}
18	17	eleq2i 2145	. . . . . . 7 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ∘ 𝐺) ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)})
19		opabid 4012	. . . . . . 7 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦)} ↔ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
20	16, 18, 19	3bitri 204	. . . . . 6 ⊢ (𝑥(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
21	20	mobii 1978	. . . . 5 ⊢ (∃*𝑦 𝑥(𝐹 ∘ 𝐺)𝑦 ↔ ∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
22	21	ralbii 2372	. . . 4 ⊢ (∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦 𝑥(𝐹 ∘ 𝐺)𝑦 ↔ ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦∃𝑧(𝑥𝐺𝑧 ∧ 𝑧𝐹𝑦))
23	15, 22	sylibr 132	. . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦 𝑥(𝐹 ∘ 𝐺)𝑦)
24		relco 4839	. . 3 ⊢ Rel (𝐹 ∘ 𝐺)
25	23, 24	jctil 305	. 2 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (Rel (𝐹 ∘ 𝐺) ∧ ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦 𝑥(𝐹 ∘ 𝐺)𝑦))
26		dffun7 4948	. 2 ⊢ (Fun (𝐹 ∘ 𝐺) ↔ (Rel (𝐹 ∘ 𝐺) ∧ ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∃*𝑦 𝑥(𝐹 ∘ 𝐺)𝑦))
27	25, 26	sylibr 132	1 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))

Syntax hints:   → wi 4   ∧ wa 102  ∀wal 1282  ∃wex 1421   ∈ wcel 1433  ∃!weu 1941  ∃*wmo 1942  ∀wral 2348   ⊆ wss 2973  ⟨cop 3401   class class class wbr 3785  {copab 3838  dom cdm 4363   ∘ ccom 4367  Rel wrel 4368  Fun wfun 4916

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786  df-opab 3840  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-fun 4924

This theorem is referenced by:  fnco  5027  f1co  5121  tposfun  5898