Theorem fssres 3657

Description: Restriction of a function with a subclass of its domain.

Assertion

Ref	Expression
fssres	|- ((F:A-->B /\ C (_ A) -> (F |` C):C-->B)

Proof of Theorem fssres

Step	Hyp	Ref	Expression
1		fnssres 3614	. . . . 5 |- ((F Fn A /\ C (_ A) -> (F |` C) Fn C)
2		resss 3397	. . . . . . 7 |- (F |` C) (_ F
3		rnss 3356	. . . . . . 7 |- ((F |` C) (_ F -> ran ( F |` C) (_ ran F)
4	2, 3	ax-mp 7	. . . . . 6 |- ran ( F |` C) (_ ran F
5		sstr 2081	. . . . . 6 |- ((ran ( F |` C) (_ ran F /\ ran F (_ B) -> ran ( F |` C) (_ B)
6	4, 5	mpan 699	. . . . 5 |- (ran F (_ B -> ran ( F |` C) (_ B)
7	1, 6	anim12i 333	. . . 4 |- (((F Fn A /\ C (_ A) /\ ran F (_ B) -> ((F |` C) Fn C /\ ran ( F |` C) (_ B))
8	7	an1rs 492	. . 3 |- (((F Fn A /\ ran F (_ B) /\ C (_ A) -> ((F |` C) Fn C /\ ran ( F |` C) (_ B))
9		df-f 3208	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
10	8, 9	sylanb 452	. 2 |- ((F:A-->B /\ C (_ A) -> ((F |` C) Fn C /\ ran ( F |` C) (_ B))
11		df-f 3208	. 2 |- ((F |` C):C-->B <-> ((F |` C) Fn C /\ ran ( F |` C) (_ B))
12	10, 11	sylibr 200	1 |- ((F:A-->B /\ C (_ A) -> (F |` C):C-->B)

Syntax hints:   -> wi 3   /\ wa 223   (_ wss 2056  ran crn 3185   |` cres 3186   Fn wfn 3191  -->wf 3192

This theorem is referenced by:  fssres2 3658  mapunen 4517  seq1rn 6505  seqzrn 6570  seq1ublem 6925  rescncf 7286  ruclem13 7537  metreslem 7831  metcnss2 7908  issubgi 8130  ghsubgi 8146  eff1i 8751  effoi 8752  hhssnv 9141

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-sep 2716  ax-pow 2756  ax-pr 2793

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-v 1819  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-nul 2290  df-pw 2412  df-sn 2422  df-pr 2423  df-op 2426  df-br 2633  df-opab 2680  df-id 2849  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-fun 3206  df-fn 3207  df-f 3208

Copyright terms: Public domain