| Parents |
| hol |
| Constants |
$  z | SETz  SETz BOOL
|
Sepz | (SETz BOOL) SETz SETz
|
 z | SETz |
Pair | SETz SETz SETz
|
 z | SETz SETz
|
$  z | SETz SETz BOOL
|
 z | SETz SETz
|
RImage | (SETz SETz) SETz SETz
|
$  z | SETz SETz SETz
|
 z | SETz SETz
|
$  z | SETz SETz SETz
|
$  z | SETz SETz SETz
|
relz | SETz BOOL
|
funz | SETz BOOL
|
domz | SETz SETz
|
ranz | SETz SETz
|
fieldz | SETz SETz
|
$z | SETz SETz SETz |
| Types |
SETz
|
| Fixity |
| Infix 230: | z | z | Infix 240: | z | z | z | Infix 250: | z |
| Axioms |
ext_axiom |   s t ( u u z s  u z t)  s = t
|
wf_axiom | p ( s ( e e z s p e) p s) ( s p s) |
separation_axiom
| p s u u z Sepz p s u z s  p u
|
pair_axiom | s t u u z Pair s t u = s  u = t
|
| z_axiom | s u u z z s ( v u z v v z s)
|
| z_axiom | s u u z z s u z s |
replacement_axiom
| f s u u z RImage f s ( v v z s u = f v)
|
| Definitions |
| z | z = Sepz ( e F) ( s T)
|
| z | s t s z t ( u u z s u z t)
|
| z | s t s z t = z (Pair s t)
|
| z | s z s = Sepz ( e t t z s e z t) (z s)
|
| z | s t s z t = Sepz ( e e z t) s
|
| z | s t s z t = Pair (Pair s t) (Pair s s)
|
relz | x relz x ( y y z x ( s t y = s z t))
|
funz | x funz x relz x ( s t u s z u z x t z u z x s = t)
|
domz | x domz x y z y z z z x) (z (z x))
|
ranz | x ranz x z y y z z z x) (z (z x))
|
fieldz | x fieldz x = domz x z ranz x
|
z | f x f z x y x z y z f y x z y z f |
| Theorems |
| z_thm | s  s z z |
set_ext_thm
| s t s = t ( u u z s u z t)
|
| z_ext_thm
| s t u u z s z t u z s u z t
|
| z_ext_thm2
| t
( x x z t) ( s s z z t ( u u z t s z u)) |
| z_ext_thm
| s t u u z s z t u z s u z t
|
pair_eq_thm
| s t u v
Pair s t = Pair u v s = u t = v s = v t = u
|
| z_eq_thm | s t u v s z t = u z v s = u t = v |
relz_ z_thm
| relz z
|
funz_ z_thm
| funz z
|
domz_ z_thm
| domz z = z
|
ranz_ z_thm
| ranz z = z
|
fieldz_ z_thm
| fieldz z = z
|
© 