Theorem writeisf ≪ | index | src | ≫ 

theorem writeisf (F: set) (a b: nat): $ isfun F -> isfun (write F a b) $;
StepHypRefExpression
1
 
x, y e. write F a b <-> ifp (x = a) (y = b) (x, y e. F)
2
 
x, z e. write F a b <-> ifp (x = a) (z = b) (x, z e. F)
3
 
x = a -> (ifp (x = a) (z = b) (x, z e. F) <-> z = b)
4
 
isfun F /\ (x = a /\ y = b) -> x = a
5
3, 4
 
isfun F /\ (x = a /\ y = b) -> (ifp (x = a) (z = b) (x, z e. F) <-> z = b)
6
 
isfun F /\ (x = a /\ y = b) -> (ifp (x = a) (z = b) (x, z e. F) -> y = z <-> z = b -> y = z)
7
 
y = b -> z = b -> y = z
8
 
isfun F /\ (x = a /\ y = b) -> y = b
9
7, 8
 
isfun F /\ (x = a /\ y = b) -> z = b -> y = z
10
6, 9
 
isfun F /\ (x = a /\ y = b) -> ifp (x = a) (z = b) (x, z e. F) -> y = z
11
2, 10
 
isfun F /\ (x = a /\ y = b) -> x, z e. write F a b -> y = z
12
 
~x = a -> (ifp (x = a) (z = b) (x, z e. F) <-> x, z e. F)
13
 
isfun F /\ (~x = a /\ x, y e. F) -> ~x = a
14
 
isfun F /\ (~x = a /\ x, y e. F) -> (ifp (x = a) (z = b) (x, z e. F) <-> x, z e. F)
15
 
isfun F /\ (~x = a /\ x, y e. F) -> (ifp (x = a) (z = b) (x, z e. F) -> y = z <-> x, z e. F -> y = z)
16
 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> isfun F
17
 
isfun F /\ (~x = a /\ x, y e. F) -> x, y e. F
18
 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> x, y e. F
19
 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> x, z e. F
20
16, 18, 19
 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> y = z
21
 
isfun F /\ (~x = a /\ x, y e. F) -> x, z e. F -> y = z
22
 
isfun F /\ (~x = a /\ x, y e. F) -> ifp (x = a) (z = b) (x, z e. F) -> y = z
23
2, 22
 
isfun F /\ (~x = a /\ x, y e. F) -> x, z e. write F a b -> y = z
24
 
isfun F -> x = a /\ y = b \/ ~x = a /\ x, y e. F -> x, z e. write F a b -> y = z
25
conv ifp
 
isfun F -> ifp (x = a) (y = b) (x, y e. F) -> x, z e. write F a b -> y = z
26
1, 25
 
isfun F -> x, y e. write F a b -> x, z e. write F a b -> y = z
27
 
isfun F -> A. z (x, y e. write F a b -> x, z e. write F a b -> y = z)
28
 
isfun F -> A. y A. z (x, y e. write F a b -> x, z e. write F a b -> y = z)
29
 
isfun F -> A. x A. y A. z (x, y e. write F a b -> x, z e. write F a b -> y = z)
30
conv isfun
 
isfun F -> isfun (write F 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)