src/ZF/Ordinal.thy
changeset 753 ec86863e87c8
parent 435 ca5356bd315a
child 852 664052e3cf66
equal deleted inserted replaced
752:b89462f9d5f1 753:ec86863e87c8
    15   Limit         :: "i=>o"
    15   Limit         :: "i=>o"
    16 
    16 
    17 translations
    17 translations
    18   "x le y"      == "x < succ(y)"
    18   "x le y"      == "x < succ(y)"
    19 
    19 
    20 rules
    20 defs
    21   Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    21   Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    22   Transset_def	"Transset(i) == ALL x:i. x<=i"
    22   Transset_def	"Transset(i) == ALL x:i. x<=i"
    23   Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
    23   Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
    24   lt_def        "i<j         == i:j & Ord(j)"
    24   lt_def        "i<j         == i:j & Ord(j)"
    25   Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    25   Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    26 
    26 
    27 
       
    28 end
    27 end