Theorem fnco 6610

Description: Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006.) (Proof shortened by AV, 20-Sep-2024.)

Assertion

Ref	Expression
fnco	⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)

Proof of Theorem fnco

Step	Hyp	Ref	Expression
1		fnfun 6592	. . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺)
2		fncofn 6609	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
3	1, 2	sylan2 593	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
4	3	3adant3 1132	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
5		cnvimassrndm 6110	. . . . 5 ⊢ (ran 𝐺 ⊆ 𝐴 → (◡𝐺 “ 𝐴) = dom 𝐺)
6	5	3ad2ant3 1135	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (◡𝐺 “ 𝐴) = dom 𝐺)
7		fndm 6595	. . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
8	7	3ad2ant2 1134	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → dom 𝐺 = 𝐵)
9	6, 8	eqtr2d 2772	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → 𝐵 = (◡𝐺 “ 𝐴))
10	9	fneq2d 6586	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → ((𝐹 ∘ 𝐺) Fn 𝐵 ↔ (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)))
11	4, 10	mpbird 257	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ⊆ wss 3901  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   “ cima 5627   ∘ ccom 5628  Fun wfun 6486   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnfco  6699  fsplitfpar  8060  fipreima  9258  updjudhcoinlf  9844  updjudhcoinrg  9845  cshco  14759  swrdco  14760  isofn  17699  prdsinvlem  18979  prdsmgp  20086  pws1  20260  frlmbas  21710  frlmup3  21755  frlmup4  21756  evlslem1  22037  upxp  23567  uptx  23569  0vfval  30681  xppreima2  32729  psgnfzto1stlem  33182  tocycfvres1  33192  tocycfvres2  33193  cycpmfvlem  33194  cycpmfv3  33197  cycpmco2  33215  sseqfv1  34546  sseqfn  34547  sseqfv2  34551  volsupnfl  37862  ftc1anclem5  37894  ftc1anclem8  37897  choicefi  45440  fourierdlem42  46389  fcoreslem4  47308  ackvalsucsucval  48930  isofnALT  49272