Theorem fnco 6657

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 6639	. . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺)
2		fncofn 6656	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
3	1, 2	sylan2 605	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
4	3	3adant3 1150	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
5		cnvimassrndm 6078	. . . . 5 ⊢ (ran 𝐺 ⊆ 𝐴 → (◡𝐺 “ 𝐴) = dom 𝐺)
6	5	3ad2ant3 1153	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (◡𝐺 “ 𝐴) = dom 𝐺)
7		fndm 6642	. . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
8	7	3ad2ant2 1152	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → dom 𝐺 = 𝐵)
9	6, 8	eqtr2d 2796	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → 𝐵 = (◡𝐺 “ 𝐴))
10	9	fneq2d 6633	. 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 1569   ⊆ wss 3895  ^◡ccnv 5649  dom cdm 5650  ran crn 5651   “ cima 5653   ∘ ccom 5654  Fun wfun 6532   Fn wfn 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541

This theorem is used by:  fnfco  6747  fsplitfpar  8131  fipreima  9350  updjudhcoinlf  10016  updjudhcoinrg  10017  cshco  14991  swrdco  14992  isofn  17955  prdsinvlem  19264  prdsmgp  20376  pws1  20559  frlmbas  22066  frlmup3  22111  frlmup4  22112  evlslem1  22396  upxp  23947  uptx  23949  0vfval  31213  xppreima2  33292  psgnfzto1stlem  33707  tocycfvres1  33717  tocycfvres2  33718  cycpmfvlem  33719  cycpmfv3  33722  cycpmco2  33740  sseqfv1  35067  sseqfn  35068  sseqfv2  35072  volsupnfl  38676  ftc1anclem5  38708  ftc1anclem8  38711  choicefi  46307  fourierdlem42  47252  fcoreslem4  48229  ackvalsucsucval  49893  isofnALT  50238