Theorem off 7697

Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)

Hypotheses

Ref	Expression
off.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
off.2	⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
off.3	⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
off.4	⊢ (𝜑 → 𝐴 ∈ 𝑉)
off.5	⊢ (𝜑 → 𝐵 ∈ 𝑊)
off.6	⊢ (𝐴 ∩ 𝐵) = 𝐶

Assertion

Ref	Expression
off	⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈)

Distinct variable groups:   𝑦,𝐺   𝑥,𝑦,𝜑   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐺(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem off

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		off.2	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
2	1	ffnd 6717	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		off.3	. . . 4 ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
4	3	ffnd 6717	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐵)
5		off.4	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6		off.5	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
7		off.6	. . 3 ⊢ (𝐴 ∩ 𝐵) = 𝐶
8		eqidd 2735	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (𝐹‘𝑧))
9		eqidd 2735	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) = (𝐺‘𝑧))
10	2, 4, 5, 6, 7, 8, 9	offval 7688	. 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑧 ∈ 𝐶 ↦ ((𝐹‘𝑧)𝑅(𝐺‘𝑧))))
11		inss1 4217	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
12	7, 11	eqsstrri 4011	. . . . 5 ⊢ 𝐶 ⊆ 𝐴
13	12	sseli 3959	. . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐴)
14		ffvelcdm 7081	. . . 4 ⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝑆)
15	1, 13, 14	syl2an 596	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐹‘𝑧) ∈ 𝑆)
16		inss2 4218	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵
17	7, 16	eqsstrri 4011	. . . . 5 ⊢ 𝐶 ⊆ 𝐵
18	17	sseli 3959	. . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵)
19		ffvelcdm 7081	. . . 4 ⊢ ((𝐺:𝐵⟶𝑇 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) ∈ 𝑇)
20	3, 18, 19	syl2an 596	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐺‘𝑧) ∈ 𝑇)
21		off.1	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
22	21	ralrimivva 3189	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
23	22	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
24		ovrspc2v 7439	. . 3 ⊢ ((((𝐹‘𝑧) ∈ 𝑆 ∧ (𝐺‘𝑧) ∈ 𝑇) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈)
25	15, 20, 23, 24	syl21anc 837	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈)
26	10, 25	fmpt3d 7116	1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050   ∩ cin 3930  ⟶wf 6537  ‘cfv 6541  (class class class)co 7413   ∘_f cof 7677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679

This theorem is referenced by:  suppofssd  8210  o1of2  15632  mndvcl  18780  ghmplusg  19833  gsumzaddlem  19908  gsumzadd  19909  lcomf  20868  frlmup1  21773  psrbagaddcl  21899  psraddcl  21913  psraddclOLD  21914  psrvscacl  21926  psrbagev1  22050  evlslem3  22053  tsmsadd  24102  mbfmulc2lem  25619  mbfaddlem  25632  i1fadd  25667  i1fmul  25668  itg1addlem4  25671  i1fmulclem  25674  i1fmulc  25675  mbfi1flimlem  25694  itg2mulclem  25718  itg2mulc  25719  itg2monolem1  25722  itg2addlem  25730  dvaddbr  25911  dvmulbr  25912  dvmulbrOLD  25913  dvaddf  25916  dvmulf  25917  dv11cn  25977  plyaddlem  26191  coeeulem  26200  coeaddlem  26225  plydivlem4  26275  jensenlem2  26968  jensen  26969  basellem7  27067  basellem9  27069  dchrmulcl  27230  ofrn  32585  offinsupp1  32674  elrgspnlem1  33190  1arithidomlem2  33504  1arithidom  33505  ply1degltdimlem  33613  fedgmullem1  33620  sibfof  34317  signshf  34578  circlemethhgt  34633  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimirlem32  37634  itg2addnc  37656  ftc1anclem3  37677  ftc1anclem6  37680  ftc1anclem8  37682  lfladdcl  39047  lflvscl  39053  fsuppssind  42582  mhphf  42586  mzpclall  42716  mzpindd  42735  expgrowth  44326  binomcxplemnotnn0  44347  dvdivcncf  45914  ofaddmndmap  48232  amgmwlem  49416