Theorem fcomptf 31852

Description: Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 7118. (Contributed by Thierry Arnoux, 30-Jun-2017.)

Hypothesis

Ref	Expression
fcomptf.1	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
fcomptf	⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥))))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷   𝑥,𝐸

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem fcomptf

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑥𝐴
2		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑥𝐷
3		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑥𝐸
4	1, 2, 3	nff 6703	. . . 4 ⊢ Ⅎ𝑥 𝐴:𝐷⟶𝐸
5		fcomptf.1	. . . . 5 ⊢ Ⅎ𝑥𝐵
6		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑥𝐶
7	5, 6, 2	nff 6703	. . . 4 ⊢ Ⅎ𝑥 𝐵:𝐶⟶𝐷
8	4, 7	nfan 1903	. . 3 ⊢ Ⅎ𝑥(𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷)
9		ffvelcdm 7071	. . . . 5 ⊢ ((𝐵:𝐶⟶𝐷 ∧ 𝑥 ∈ 𝐶) → (𝐵‘𝑥) ∈ 𝐷)
10	9	adantll 713	. . . 4 ⊢ (((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) ∧ 𝑥 ∈ 𝐶) → (𝐵‘𝑥) ∈ 𝐷)
11	10	ex 414	. . 3 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝑥 ∈ 𝐶 → (𝐵‘𝑥) ∈ 𝐷))
12	8, 11	ralrimi 3255	. 2 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → ∀𝑥 ∈ 𝐶 (𝐵‘𝑥) ∈ 𝐷)
13		ffn 6707	. . . 4 ⊢ (𝐵:𝐶⟶𝐷 → 𝐵 Fn 𝐶)
14	13	adantl 483	. . 3 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐵 Fn 𝐶)
15	5	dffn5f 6952	. . 3 ⊢ (𝐵 Fn 𝐶 ↔ 𝐵 = (𝑥 ∈ 𝐶 ↦ (𝐵‘𝑥)))
16	14, 15	sylib 217	. 2 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐵 = (𝑥 ∈ 𝐶 ↦ (𝐵‘𝑥)))
17		ffn 6707	. . . 4 ⊢ (𝐴:𝐷⟶𝐸 → 𝐴 Fn 𝐷)
18	17	adantr 482	. . 3 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐴 Fn 𝐷)
19		dffn5 6940	. . 3 ⊢ (𝐴 Fn 𝐷 ↔ 𝐴 = (𝑦 ∈ 𝐷 ↦ (𝐴‘𝑦)))
20	18, 19	sylib 217	. 2 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐴 = (𝑦 ∈ 𝐷 ↦ (𝐴‘𝑦)))
21		fveq2 6881	. 2 ⊢ (𝑦 = (𝐵‘𝑥) → (𝐴‘𝑦) = (𝐴‘(𝐵‘𝑥)))
22	12, 16, 20, 21	fmptcof 7115	1 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥))))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Ⅎwnfc 2884   ↦ cmpt 5227   ∘ ccom 5676   Fn wfn 6530  ⟶wf 6531  ‘cfv 6535

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-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5295  ax-nul 5302  ax-pr 5423

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-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-br 5145  df-opab 5207  df-mpt 5228  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-fv 6543

This theorem is referenced by:  ofoprabco  31858