Theorem writeArrow ≪ | index | src | ≫ 

theorem writeArrow (A B: set) (G: wff) (a b f g: nat):
  $ G -> f e. Arrow A B $ >
  $ G -> a e. A $ >
  $ G -> b e. B $ >
  $ G -> write f a b == g $ >
  $ G -> g e. Arrow A B $;
StepHypRefExpression
1 elArrow 
g e. Arrow A B <-> func g A B
2 hyp h 
G -> write f a b == g
3 2 isfeqd 
G -> (isfun (write f a b) <-> isfun g)
4 writeisf 
isfun f -> isfun (write f a b)
5 Arrowisf 
f e. Arrow A B -> isfun f
6 hyp hf 
G -> f e. Arrow A B
7 5, 6 syl 
G -> isfun f
8 4, 7 syl 
G -> isfun (write f a b)
9 3, 8 mpbid 
G -> isfun g
10 2 dmeqd 
G -> Dom (write f a b) == Dom g
11 dmwrite 
Dom (write f a b) == Dom f u. sn a
12 Arrowdm 
f e. Arrow A B -> Dom f == A
13 12, 6 syl 
G -> Dom f == A
14 13 uneq1d 
G -> Dom f u. sn a == A u. sn a
15 equn2 
sn a C_ A <-> A u. sn a == A
16 snss 
sn a C_ A <-> a e. A
17 hyp ha 
G -> a e. A
18 16, 17 sylibr 
G -> sn a C_ A
19 15, 18 sylib 
G -> A u. sn a == A
20 14, 19 eqstrd 
G -> Dom f u. sn a == A
21 11, 20 syl5eqs 
G -> Dom (write f a b) == A
22 10, 21 eqstr3d 
G -> Dom g == A
23 9, 22 iand 
G -> isfun g /\ Dom g == A
24 2 rneqd 
G -> Ran (write f a b) == Ran g
25 24 sseq1d 
G -> (Ran (write f a b) C_ B <-> Ran g C_ B)
26 sstr 
Ran (write f a b) C_ Ran f u. sn b -> Ran f u. sn b C_ B -> Ran (write f a b) C_ B
27 rnwrite 
Ran (write f a b) C_ Ran f u. sn b
28 26, 27 ax_mp 
Ran f u. sn b C_ B -> Ran (write f a b) C_ B
29 unss 
Ran f u. sn b C_ B <-> Ran f C_ B /\ sn b C_ B
30 Arrowrn 
f e. Arrow A B -> Ran f C_ B
31 30, 6 syl 
G -> Ran f C_ B
32 snss 
sn b C_ B <-> b e. B
33 hyp hb 
G -> b e. B
34 32, 33 sylibr 
G -> sn b C_ B
35 31, 34 iand 
G -> Ran f C_ B /\ sn b C_ B
36 29, 35 sylibr 
G -> Ran f u. sn b C_ B
37 28, 36 syl 
G -> Ran (write f a b) C_ B
38 25, 37 mpbid 
G -> Ran g C_ B
39 23, 38 iand 
G -> isfun g /\ Dom g == A /\ Ran g C_ B
40 39 conv func 
G -> func g A B
41 1, 40 sylibr 
G -> g e. Arrow A 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)