The Theory zfc

Parents

Children

Constants

$z	SETz SETz BOOL
z	SETz
Sepz	(SETz BOOL) SETz SETz
Pair	SETz SETz SETz
z	SETz SETz
$z	SETz SETz SETz
z	SETz SETz
$z	SETz SETz SETz
relz	SETz BOOL
funz	SETz BOOL
domz	SETz SETz
ranz	SETz SETz
fieldz	SETz SETz

Types

Fixity

Infix 230:	z
Infix 240:	z	z

Axioms

ext_axiom	s t ( u u z s u z t) s = t
z_axiom	s s z z
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)

Definitions

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 = 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
	= Sepz ( y z y z z z x) (z (z x))
ranz	x
	ranz x
	= Sepz ( z y y z z z x) (z (z x))
fieldz	x fieldz x = domz x z ranz x

Theorems

set_ext_thm	s t s = t ( u 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

---

© created 1999/10/29 modified 1999/11/02