Theorem funcres ≪ | index | src | ≫ 

theorem funcres (A B C F: set): $ func F A B /\ C C_ A -> func (F |` C) C B $;
StepHypRefExpression
1 resisf 
isfun F -> isfun (F |` C)
2 funcisf 
func F A B -> isfun F
3 2 anwl 
func F A B /\ C C_ A -> isfun F
4 1, 3 syl 
func F A B /\ C C_ A -> isfun (F |` C)
5 dmres 
Dom (F |` C) == Dom F i^i C
6 eqin2 
C C_ Dom F <-> Dom F i^i C == C
7 funcdm 
func F A B -> Dom F == A
8 7 sseq2d 
func F A B -> (C C_ Dom F <-> C C_ A)
9 8 bi2d 
func F A B -> C C_ A -> C C_ Dom F
10 9 imp 
func F A B /\ C C_ A -> C C_ Dom F
11 6, 10 sylib 
func F A B /\ C C_ A -> Dom F i^i C == C
12 5, 11 syl5eqs 
func F A B /\ C C_ A -> Dom (F |` C) == C
13 4, 12 iand 
func F A B /\ C C_ A -> isfun (F |` C) /\ Dom (F |` C) == C
14 sstr 
Ran (F |` C) C_ Ran F -> Ran F C_ B -> Ran (F |` C) C_ B
15 rnss 
F |` C C_ F -> Ran (F |` C) C_ Ran F
16 resss 
F |` C C_ F
17 15, 16 ax_mp 
Ran (F |` C) C_ Ran F
18 14, 17 ax_mp 
Ran F C_ B -> Ran (F |` C) C_ B
19 funcrn 
func F A B -> Ran F C_ B
20 19 anwl 
func F A B /\ C C_ A -> Ran F C_ B
21 18, 20 syl 
func F A B /\ C C_ A -> Ran (F |` C) C_ B
22 13, 21 iand 
func F A B /\ C C_ A -> isfun (F |` C) /\ Dom (F |` C) == C /\ Ran (F |` C) C_ B
23 22 conv func 
func F A B /\ C C_ A -> func (F |` C) C B

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)