UP

The Theory zfc

Parents

hol

Children

pf

Constants

$memberofzSETz func1 SETz func1 BOOL
emptysetzSETz
Sepz(SETz func1 BOOL) func1 SETz func1 SETz
PairSETz func1 SETz func1 SETz
lcupzSETz func1 SETz
$scupzSETz func1 SETz func1 SETz
lcapzSETz func1 SETz
$mapstozSETz func1 SETz func1 SETz
relzSETz func1 BOOL
funzSETz func1 BOOL
domzSETz func1 SETz
ranzSETz func1 SETz
fieldzSETz func1 SETz

Types

SETz

Fixity

Infix 230:memberofz
Infix 240:scupzmapstoz

Axioms

ext_axiomturnstil forall s tspot (forall uspot u memberofz s equiv u memberofz t) implies s = t
emptysetz_axiomturnstil forall sspot not s memberofz emptysetz
separation_axiom turnstil forall p s uspot u memberofz Sepz p s equiv u memberofz s and p u
pair_axiomturnstil forall s t uspot u memberofz Pair s t equiv u = s or u = t
lcupz_axiomturnstil forall s uspot u memberofz lcupz s equiv (exists vspot u memberofz v and v memberofz s)

Definitions

scupzturnstil forall s tspot s scupz t = lcupz (Pair s t)
lcapzturnstil forall s
spot lcapz s = Sepz (lambda espot forall tspot t memberofz s implies e memberofz t) (lcupz s)
mapstozturnstil forall s tspot s mapstoz t = Pair (Pair s t) (Pair s s)
relzturnstil forall xspot relz x equiv (forall yspot y memberofz x implies (exists s tspot y = s mapstoz t))
funzturnstil forall x
spot funz x
equiv relz x
and (forall s t u
spot s mapstoz u memberofz x and t mapstoz u memberofz x implies s = t)
domzturnstil forall x
spot domz x
= Sepz (lambda yspot exists zspot y mapstoz z memberofz x) (lcupz (lcupz x))
ranzturnstil forall x
spot ranz x
= Sepz (lambda zspot exists yspot y mapstoz z memberofz x) (lcupz (lcupz x))
fieldzturnstil forall xspot fieldz x = domz x scupz ranz x

Theorems

set_ext_thm turnstil forall s tspot s = t equiv (forall uspot u memberofz s equiv u memberofz t)
pair_eq_thm turnstil forall s t u v
spot Pair s t = Pair u v equiv s = u and t = v or s = v and t = u
mapstoz_eq_thmturnstil forall s t u vspot s mapstoz t = u mapstoz v equiv s = u and t = v


HOME net links © RBJ created 1999/10/29 modified 1999/11/02