Theorem dmwrite ≪ | index | src | ≫ 

theorem dmwrite (F: set) (a b: nat): $ Dom (write F a b) == Dom F u. sn a $;
StepHypRefExpression
1 bitr4 
(x e. Dom (write F a b) <-> x = a \/ x e. Dom F) -> (x e. Dom F u. sn a <-> x = a \/ x e. Dom F) -> (x e. Dom (write F a b) <-> x e. Dom F u. sn a)
2 eldm 
x e. Dom (write F a b) <-> E. y x, y e. write F a b
3 elwrite 
x, y e. write F a b <-> ifp (x = a) (y = b) (x, y e. F)
4 preldm 
x, y e. F -> x e. Dom F
5 ifpneg 
~x = a -> (ifp (x = a) (y = b) (x, y e. F) <-> x, y e. F)
6 5 bi1d 
~x = a -> ifp (x = a) (y = b) (x, y e. F) -> x, y e. F
7 4, 6 syl6 
~x = a -> ifp (x = a) (y = b) (x, y e. F) -> x e. Dom F
8 7 com12 
ifp (x = a) (y = b) (x, y e. F) -> ~x = a -> x e. Dom F
9 8 conv or 
ifp (x = a) (y = b) (x, y e. F) -> x = a \/ x e. Dom F
10 3, 9 sylbi 
x, y e. write F a b -> x = a \/ x e. Dom F
11 10 eex 
E. y x, y e. write F a b -> x = a \/ x e. Dom F
12 2, 11 sylbi 
x e. Dom (write F a b) -> x = a \/ x e. Dom F
13 preldm 
x, b e. write F a b -> x e. Dom (write F a b)
14 elwrite 
x, b e. write F a b <-> ifp (x = a) (b = b) (x, b e. F)
15 eqid 
b = b
16 ifppos 
x = a -> (ifp (x = a) (b = b) (x, b e. F) <-> b = b)
17 15, 16 mpbiri 
x = a -> ifp (x = a) (b = b) (x, b e. F)
18 14, 17 sylibr 
x = a -> x, b e. write F a b
19 13, 18 syl 
x = a -> x e. Dom (write F a b)
20 19 a1i 
x = a \/ x e. Dom F -> x = a -> x e. Dom (write F a b)
21 eldm 
x e. Dom F <-> E. y x, y e. F
22 preldm 
x, y e. write F a b -> x e. Dom (write F a b)
23 3, 5 syl5bb 
~x = a -> (x, y e. write F a b <-> x, y e. F)
24 23 imeq1d 
~x = a -> (x, y e. write F a b -> x e. Dom (write F a b) <-> x, y e. F -> x e. Dom (write F a b))
25 22, 24 mpbii 
~x = a -> x, y e. F -> x e. Dom (write F a b)
26 25 eexd 
~x = a -> E. y x, y e. F -> x e. Dom (write F a b)
27 21, 26 syl5bi 
~x = a -> x e. Dom F -> x e. Dom (write F a b)
28 27 a2i 
(~x = a -> x e. Dom F) -> ~x = a -> x e. Dom (write F a b)
29 28 conv or 
x = a \/ x e. Dom F -> ~x = a -> x e. Dom (write F a b)
30 20, 29 casesd 
x = a \/ x e. Dom F -> x e. Dom (write F a b)
31 12, 30 ibii 
x e. Dom (write F a b) <-> x = a \/ x e. Dom F
32 1, 31 ax_mp 
(x e. Dom F u. sn a <-> x = a \/ x e. Dom F) -> (x e. Dom (write F a b) <-> x e. Dom F u. sn a)
33 bitr 
(x e. Dom F u. sn a <-> x e. Dom F \/ x e. sn a) -> (x e. Dom F \/ x e. sn a <-> x = a \/ x e. Dom F) -> (x e. Dom F u. sn a <-> x = a \/ x e. Dom F)
34 elun 
x e. Dom F u. sn a <-> x e. Dom F \/ x e. sn a
35 33, 34 ax_mp 
(x e. Dom F \/ x e. sn a <-> x = a \/ x e. Dom F) -> (x e. Dom F u. sn a <-> x = a \/ x e. Dom F)
36 bitr 
(x e. Dom F \/ x e. sn a <-> x e. sn a \/ x e. Dom F) -> (x e. sn a \/ x e. Dom F <-> x = a \/ x e. Dom F) -> (x e. Dom F \/ x e. sn a <-> x = a \/ x e. Dom F)
37 orcomb 
x e. Dom F \/ x e. sn a <-> x e. sn a \/ x e. Dom F
38 36, 37 ax_mp 
(x e. sn a \/ x e. Dom F <-> x = a \/ x e. Dom F) -> (x e. Dom F \/ x e. sn a <-> x = a \/ x e. Dom F)
39 oreq1 
(x e. sn a <-> x = a) -> (x e. sn a \/ x e. Dom F <-> x = a \/ x e. Dom F)
40 elsn 
x e. sn a <-> x = a
41 39, 40 ax_mp 
x e. sn a \/ x e. Dom F <-> x = a \/ x e. Dom F
42 38, 41 ax_mp 
x e. Dom F \/ x e. sn a <-> x = a \/ x e. Dom F
43 35, 42 ax_mp 
x e. Dom F u. sn a <-> x = a \/ x e. Dom F
44 32, 43 ax_mp 
x e. Dom (write F a b) <-> x e. Dom F u. sn a
45 44 eqri 
Dom (write F a b) == Dom F u. sn a

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)