Theorem writeself ≪ | index | src | ≫ 

theorem writeself (F: set) (a: nat):
  $ isfun F /\ a e. Dom F -> write F a (F @ a) == F $;
StepHypRefExpression
1 elwrite 
x, y e. write F a (F @ a) <-> ifp (x = a) (y = F @ a) (x, y e. F)
2 ifppos 
x = a -> (ifp (x = a) (y = F @ a) (x, y e. F) <-> y = F @ a)
3 anr 
isfun F /\ a e. Dom F /\ x = a -> x = a
4 2, 3 syl 
isfun F /\ a e. Dom F /\ x = a -> (ifp (x = a) (y = F @ a) (x, y e. F) <-> y = F @ a)
5 preq1 
x = a -> x, y = a, y
6 5, 3 syl 
isfun F /\ a e. Dom F /\ x = a -> x, y = a, y
7 6 eleq1d 
isfun F /\ a e. Dom F /\ x = a -> (x, y e. F <-> a, y e. F)
8 isfappb 
isfun F -> (a, y e. F <-> a e. Dom F /\ F @ a = y)
9 anll 
isfun F /\ a e. Dom F /\ x = a -> isfun F
10 8, 9 syl 
isfun F /\ a e. Dom F /\ x = a -> (a, y e. F <-> a e. Dom F /\ F @ a = y)
11 7, 10 bitrd 
isfun F /\ a e. Dom F /\ x = a -> (x, y e. F <-> a e. Dom F /\ F @ a = y)
12 bian1 
a e. Dom F -> (a e. Dom F /\ F @ a = y <-> F @ a = y)
13 anlr 
isfun F /\ a e. Dom F /\ x = a -> a e. Dom F
14 12, 13 syl 
isfun F /\ a e. Dom F /\ x = a -> (a e. Dom F /\ F @ a = y <-> F @ a = y)
15 11, 14 bitrd 
isfun F /\ a e. Dom F /\ x = a -> (x, y e. F <-> F @ a = y)
16 eqcomb 
F @ a = y <-> y = F @ a
17 16 a1i 
isfun F /\ a e. Dom F /\ x = a -> (F @ a = y <-> y = F @ a)
18 15, 17 bitrd 
isfun F /\ a e. Dom F /\ x = a -> (x, y e. F <-> y = F @ a)
19 18 bicomd 
isfun F /\ a e. Dom F /\ x = a -> (y = F @ a <-> x, y e. F)
20 4, 19 bitrd 
isfun F /\ a e. Dom F /\ x = a -> (ifp (x = a) (y = F @ a) (x, y e. F) <-> x, y e. F)
21 1, 20 syl5bb 
isfun F /\ a e. Dom F /\ x = a -> (x, y e. write F a (F @ a) <-> x, y e. F)
22 ifpneg 
~x = a -> (ifp (x = a) (y = F @ a) (x, y e. F) <-> x, y e. F)
23 anr 
isfun F /\ a e. Dom F /\ ~x = a -> ~x = a
24 22, 23 syl 
isfun F /\ a e. Dom F /\ ~x = a -> (ifp (x = a) (y = F @ a) (x, y e. F) <-> x, y e. F)
25 1, 24 syl5bb 
isfun F /\ a e. Dom F /\ ~x = a -> (x, y e. write F a (F @ a) <-> x, y e. F)
26 21, 25 casesda 
isfun F /\ a e. Dom F -> (x, y e. write F a (F @ a) <-> x, y e. F)
27 26 eqrd2 
isfun F /\ a e. Dom F -> write F a (F @ a) == F

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)