Theorem writeres ≪ | index | src | ≫ 

theorem writeres (F: set) (a b: nat) {x: nat}:
  $ write F a b == (F |` {x | x != a}) u. sn (a, b) $;
StepHypRefExpression
1 bitr3 
(fst p, snd p e. write F a b <-> p e. write F a b) ->
  (fst p, snd p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b)) ->
  (p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b))
2 eleq1 
fst p, snd p = p -> (fst p, snd p e. write F a b <-> p e. write F a b)
3 fstsnd 
fst p, snd p = p
4 2, 3 ax_mp 
fst p, snd p e. write F a b <-> p e. write F a b
5 1, 4 ax_mp 
(fst p, snd p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b)) -> (p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b))
6 bitr 
(fst p, snd p e. write F a b <-> ifp (fst p = a) (snd p = b) (fst p, snd p e. F)) ->
  (ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> p e. (F |` {x | x != a}) u. sn (a, b)) ->
  (fst p, snd p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b))
7 elwrite 
fst p, snd p e. write F a b <-> ifp (fst p = a) (snd p = b) (fst p, snd p e. F)
8 6, 7 ax_mp 
(ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> p e. (F |` {x | x != a}) u. sn (a, b)) ->
  (fst p, snd p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b))
9 bitr 
(ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> ~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b) ->
  (~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> p e. (F |` {x | x != a}) u. sn (a, b)) ->
  (ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> p e. (F |` {x | x != a}) u. sn (a, b))
10 orcomb 
fst p = a /\ snd p = b \/ ~fst p = a /\ fst p, snd p e. F <-> ~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b
11 10 conv ifp 
ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> ~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b
12 9, 11 ax_mp 
(~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> p e. (F |` {x | x != a}) u. sn (a, b)) ->
  (ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> p e. (F |` {x | x != a}) u. sn (a, b))
13 bitr4 
(~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> p e. (F |` {x | x != a}) u. sn (a, b))
14 oreq1 
(~fst p = a /\ fst p, snd p e. F <-> fst p, snd p e. F /\ fst p e. {x | x != a}) ->
  (~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
15 bitr4 
(~fst p = a /\ fst p, snd p e. F <-> fst p, snd p e. F /\ ~fst p = a) ->
  (fst p, snd p e. F /\ fst p e. {x | x != a} <-> fst p, snd p e. F /\ ~fst p = a) ->
  (~fst p = a /\ fst p, snd p e. F <-> fst p, snd p e. F /\ fst p e. {x | x != a})
16 ancomb 
~fst p = a /\ fst p, snd p e. F <-> fst p, snd p e. F /\ ~fst p = a
17 15, 16 ax_mp 
(fst p, snd p e. F /\ fst p e. {x | x != a} <-> fst p, snd p e. F /\ ~fst p = a) ->
  (~fst p = a /\ fst p, snd p e. F <-> fst p, snd p e. F /\ fst p e. {x | x != a})
18 neeq1 
x = fst p -> (x != a <-> fst p != a)
19 18 conv ne 
x = fst p -> (x != a <-> ~fst p = a)
20 19 elabe 
fst p e. {x | x != a} <-> ~fst p = a
21 20 aneq2i 
fst p, snd p e. F /\ fst p e. {x | x != a} <-> fst p, snd p e. F /\ ~fst p = a
22 17, 21 ax_mp 
~fst p = a /\ fst p, snd p e. F <-> fst p, snd p e. F /\ fst p e. {x | x != a}
23 14, 22 ax_mp 
~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b
24 13, 23 ax_mp 
(p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> p e. (F |` {x | x != a}) u. sn (a, b))
25 bitr3 
(fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> p e. (F |` {x | x != a}) u. sn (a, b)) ->
  (fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
26 eleq1 
fst p, snd p = p -> (fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> p e. (F |` {x | x != a}) u. sn (a, b))
27 26, 3 ax_mp 
fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> p e. (F |` {x | x != a}) u. sn (a, b)
28 25, 27 ax_mp 
(fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
29 bitr 
(fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b)) ->
  (fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
30 elun 
fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b)
31 29, 30 ax_mp 
(fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b) ->
  (fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
32 oreq 
(fst p, snd p e. F |` {x | x != a} <-> fst p, snd p e. F /\ fst p e. {x | x != a}) ->
  (fst p, snd p e. sn (a, b) <-> fst p = a /\ snd p = b) ->
  (fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
33 prelres 
fst p, snd p e. F |` {x | x != a} <-> fst p, snd p e. F /\ fst p e. {x | x != a}
34 32, 33 ax_mp 
(fst p, snd p e. sn (a, b) <-> fst p = a /\ snd p = b) ->
  (fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b)
35 bitr 
(fst p, snd p e. sn (a, b) <-> fst p, snd p = a, b) ->
  (fst p, snd p = a, b <-> fst p = a /\ snd p = b) ->
  (fst p, snd p e. sn (a, b) <-> fst p = a /\ snd p = b)
36 elsn 
fst p, snd p e. sn (a, b) <-> fst p, snd p = a, b
37 35, 36 ax_mp 
(fst p, snd p = a, b <-> fst p = a /\ snd p = b) -> (fst p, snd p e. sn (a, b) <-> fst p = a /\ snd p = b)
38 prth 
fst p, snd p = a, b <-> fst p = a /\ snd p = b
39 37, 38 ax_mp 
fst p, snd p e. sn (a, b) <-> fst p = a /\ snd p = b
40 34, 39 ax_mp 
fst p, snd p e. F |` {x | x != a} \/ fst p, snd p e. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b
41 31, 40 ax_mp 
fst p, snd p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b
42 28, 41 ax_mp 
p e. (F |` {x | x != a}) u. sn (a, b) <-> fst p, snd p e. F /\ fst p e. {x | x != a} \/ fst p = a /\ snd p = b
43 24, 42 ax_mp 
~fst p = a /\ fst p, snd p e. F \/ fst p = a /\ snd p = b <-> p e. (F |` {x | x != a}) u. sn (a, b)
44 12, 43 ax_mp 
ifp (fst p = a) (snd p = b) (fst p, snd p e. F) <-> p e. (F |` {x | x != a}) u. sn (a, b)
45 8, 44 ax_mp 
fst p, snd p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b)
46 5, 45 ax_mp 
p e. write F a b <-> p e. (F |` {x | x != a}) u. sn (a, b)
47 46 eqri 
write F a b == (F |` {x | x != a}) u. sn (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)