Theorem rnwrite ≪ | index | src | ≫ 

theorem rnwrite (F: set) (a b: nat): $ Ran (write F a b) C_ Ran F u. sn b $;
StepHypRefExpression
1 elrn 
x e. Ran (write F a b) <-> E. y y, x e. write F a b
2 elwrite 
y, x e. write F a b <-> ifp (y = a) (x = b) (y, x e. F)
3 eor 
(y = a /\ x = b -> x e. Ran F u. sn b) -> (~y = a /\ y, x e. F -> x e. Ran F u. sn b) -> y = a /\ x = b \/ ~y = a /\ y, x e. F -> x e. Ran F u. sn b
4 3 conv ifp 
(y = a /\ x = b -> x e. Ran F u. sn b) -> (~y = a /\ y, x e. F -> x e. Ran F u. sn b) -> ifp (y = a) (x = b) (y, x e. F) -> x e. Ran F u. sn b
5 elun2 
x e. sn b -> x e. Ran F u. sn b
6 elsn 
x e. sn b <-> x = b
7 anr 
y = a /\ x = b -> x = b
8 6, 7 sylibr 
y = a /\ x = b -> x e. sn b
9 5, 8 syl 
y = a /\ x = b -> x e. Ran F u. sn b
10 4, 9 ax_mp 
(~y = a /\ y, x e. F -> x e. Ran F u. sn b) -> ifp (y = a) (x = b) (y, x e. F) -> x e. Ran F u. sn b
11 elun1 
x e. Ran F -> x e. Ran F u. sn b
12 prelrn 
y, x e. F -> x e. Ran F
13 12 anwr 
~y = a /\ y, x e. F -> x e. Ran F
14 11, 13 syl 
~y = a /\ y, x e. F -> x e. Ran F u. sn b
15 10, 14 ax_mp 
ifp (y = a) (x = b) (y, x e. F) -> x e. Ran F u. sn b
16 2, 15 sylbi 
y, x e. write F a b -> x e. Ran F u. sn b
17 16 eex 
E. y y, x e. write F a b -> x e. Ran F u. sn b
18 1, 17 sylbi 
x e. Ran (write F a b) -> x e. Ran F u. sn b
19 18 ax_gen 
A. x (x e. Ran (write F a b) -> x e. Ran F u. sn b)
20 19 conv subset 
Ran (write F a b) C_ Ran F u. sn 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)