Theorem fnco 6660

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 6642	. . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺)
2		fncofn 6659	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
3	1, 2	sylan2 605	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
4	3	3adant3 1150	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
5		cnvimassrndm 6154	. . . . 5 ⊢ (ran 𝐺 ⊆ 𝐴 → (◡𝐺 “ 𝐴) = dom 𝐺)
6	5	3ad2ant3 1153	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (◡𝐺 “ 𝐴) = dom 𝐺)
7		fndm 6645	. . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
8	7	3ad2ant2 1152	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → dom 𝐺 = 𝐵)
9	6, 8	eqtr2d 2802	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → 𝐵 = (◡𝐺 “ 𝐴))
10	9	fneq2d 6636	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → ((𝐹 ∘ 𝐺) Fn 𝐵 ↔ (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)))
11	4, 10	mpbird 260	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ⊆ wss 3908  ^◡ccnv 5665  dom cdm 5666  ran crn 5667   “ cima 5669   ∘ ccom 5670  Fun wfun 6537   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-fun 6545  df-fn 6546

This theorem is used by:  fnfco  6750  fsplitfpar  8122  fipreima  9325  updjudhcoinlf  9937  updjudhcoinrg  9938  cshco  14899  swrdco  14900  isofn  17857  prdsinvlem  19146  prdsmgp  20258  pws1  20439  frlmbas  21942  frlmup3  21987  frlmup4  21988  evlslem1  22270  upxp  23817  uptx  23819  0vfval  30995  xppreima2  33033  psgnfzto1stlem  33451  tocycfvres1  33461  tocycfvres2  33462  cycpmfvlem  33463  cycpmfv3  33466  cycpmco2  33484  sseqfv1  34811  sseqfn  34812  sseqfv2  34816  volsupnfl  38357  ftc1anclem5  38389  ftc1anclem8  38392  choicefi  45958  fourierdlem42  46904  fcoreslem4  47844  ackvalsucsucval  49509  isofnALT  49850