Basic Constants, Axioms, Definitions and Claims
Download fileconst in:V>V>*;
const eq:V>V>*;
const not:*>*;
const imp:*>*>*;
const equiv:*>*>*;
const and:*>*>*;
const or:*>*>*;
const all:(V>*)>*;
const ex:(V>*)>*;
const exu:(V>*)>*;
known eqE:!x:V.!y:V.!phi:V>*.eq x y>phi x>phi y;
known xmcases:!phi:*.!psi:*.(phi>psi)>(not phi>psi)>psi;
known notE:!phi:*.!psi:*.phi>not phi>psi;
known impI:!phi:*.!psi:*.(phi>psi)>imp phi psi;
known impE:!phi:*.!psi:*.imp phi psi>phi>psi;
known equivI1:!phi:*.!psi:*.phi>psi>equiv phi psi;
known equivI2:!phi:*.!psi:*.not phi>not psi>equiv phi psi;
known equivEimp1:!phi:*.!psi:*.equiv phi psi>phi>psi;
known equivEimp2:!phi:*.!psi:*.equiv phi psi>psi>phi;
known andEquiv:!phi:*.!psi:*.equiv (and phi psi) (not (imp phi (not psi)));
known orEquiv:!phi:*.!psi:*.equiv (or phi psi) (imp (not phi) psi);
known allI:!phi:V>*.(!x:V.phi x)>all (\x.phi x);
known allE:!phi:V>*.all (\x.phi x)>!x:V.phi x;
known exEquiv:!phi:V>*.equiv (ex (\x.phi x)) (not (all (\x.not (phi x))));
known exuEquiv:!phi:V>*.equiv (exu (\x.phi x)) (ex (\x.and (phi x) (all (\y.imp (phi y) (eq x y)))));
known setextAx:all (\A.all (\B.imp (all (\x.equiv (in x A) (in x B))) (eq A B)));
const emptyset:V;
known emptysetAx:all (\x.not (in x emptyset));
const setadjoin:V>V>V;
known setadjoinAx:all (\x.all (\A.all (\y.equiv (in y (setadjoin x A)) (or (eq y x) (in y A)))));
const powerset:V>V;
known powersetAx:all (\A.all (\B.equiv (in B (powerset A)) (all (\x.imp (in x B) (in x A)))));
const setunion:V>V;
known setunionAx:all (\A.all (\x.equiv (in x (setunion A)) (ex (\B.and (in x B) (in B A)))));
const omega:V;
known omega0Ax:in emptyset omega;
known omegaSAx:all (\x.imp (in x omega) (in (setadjoin x x) omega));
known omegaIndAx:all (\A.imp (and (in emptyset A) (all (\x.imp (and (in x omega) (in x A)) (in (setadjoin x x) A)))) (all (\x.imp (in x omega) (in x A))));
known replAx:!phi:V>V>*.all (\A.imp (all (\x.imp (in x A) (exu (\y.phi x y)))) (ex (\B.all (\x.equiv (in x B) (ex (\y.and (in y A) (phi y x)))))));
known foundationAx:all (\A.imp (ex (\x.in x A)) (ex (\B.and (in B A) (not (ex (\x.and (in x B) (in x A)))))));
known wellorderingAx:all (\A.ex (\B.and (and (and (all (\C.imp (in C B) (all (\x.imp (in x C) (in x A))))) (all (\x.all (\y.imp (and (in x A) (in y A)) (imp (all (\C.imp (in C B) (equiv (in x C) (in y C)))) (eq x y)))))) (all (\C.all (\D.imp (and (in C B) (in D B)) (or (all (\x.imp (in x C) (in x D))) (all (\x.imp (in x D) (in x C)))))))) (all (\C.imp (and (all (\x.imp (in x C) (in x A))) (ex (\x.in x C))) (ex (\D.ex (\x.and (and (and (in D B) (in x C)) (not (ex (\y.and (in y D) (in y C))))) (all (\E.imp (in E B) (or (all (\y.imp (in y E) (in y D))) (in x E)))))))))));
const descr:(V>*)>V;
known descrp:!phi:V>*.exu (\x.phi x)>phi (descr (\x.phi x));
const dsetconstr:V>(V>*)>V;
known dsetconstrI:!A:V.!phi:V>*.!a:V.in a A>phi a>in a (dsetconstr A (\b.phi b));
known dsetconstrEL:!A:V.!phi:V>*.!x:V.in x (dsetconstr A (\a.phi a))>in x A;
known dsetconstrERa:!A:V.!phi:V>*.!a:V.in a A>in a (dsetconstr A (\b.phi b))>phi a;
claim dsetconstrER:!A:V.!phi:V>*.!x:V.in x (dsetconstr A (\a.phi a))>phi x; (proof)
def dall:V>(V>*)>*=\A.\phi.eq (dsetconstr A (\a.phi a)) A;
def dex:V>(V>*)>*=\A.\phi.not (eq (dsetconstr A (\a.phi a)) emptyset);
def prop2set:*>V=\phi.dsetconstr (powerset emptyset) (\x.phi);
claim prop2setE:!phi:*.!x:V.in x (prop2set phi)>phi; (proof)
def dand:*>*>*=\phi.\psi.dex (prop2set phi) (\x.psi);
def dimp:*>*>*=\phi.\psi.dall (prop2set phi) (\x.psi);
def false:*=in emptyset emptyset;
claim emptysetE:!x:V.in x emptyset>!phi:*.phi; (proof)
claim falseE:!phi:*.false>phi; (proof)
claim notI:!phi:*.(phi>false)>not phi; (proof)
claim contradiction:!phi:*.(not phi>false)>phi; (proof)
claim dnegE:!phi:*.not (not phi)>phi; (proof)
claim dnegI:!phi:*.phi>not (not phi); (proof)
claim contrapositive1:!phi:*.!psi:*.(phi>psi)>not psi>not phi; (proof)
claim contrapositive2:!phi:*.!psi:*.(not phi>psi)>not psi>phi; (proof)
claim contrapositive3:!phi:*.!psi:*.(not phi>not psi)>psi>phi; (proof)
claim contrapositive4:!phi:*.!psi:*.(phi>not psi)>psi>not phi; (proof)
claim andI:!phi:*.!psi:*.phi>psi>and phi psi; (proof)
claim andEL:!phi:*.!psi:*.and phi psi>phi; (proof)
claim andER:!phi:*.!psi:*.and phi psi>psi; (proof)
claim orIL:!phi:*.!psi:*.phi>or phi psi; (proof)
claim orIR:!phi:*.!psi:*.psi>or phi psi; (proof)
claim orE:!phi:*.!psi:*.or phi psi>!theta:*.(phi>theta)>(psi>theta)>theta; (proof)
claim orIDemorgan:!phi:*.!psi:*.(not phi>not psi>false)>or phi psi; (proof)
claim exE:!phi:V>*.ex (\x.phi x)>!psi:*.(!x:V.phi x>psi)>psi; (proof)
claim exI:!phi:V>*.!x:V.phi x>ex (\y.phi y); (proof)
claim equivI:!phi:*.!psi:*.(phi>psi)>(psi>phi)>equiv phi psi; (proof)
claim equivE:!phi:*.!psi:*.!theta:*.equiv phi psi>(phi>psi>theta)>(not phi>not psi>theta)>theta; (proof)
claim setext:!A:V.!B:V.(!x:V.in x A>in x B)>(!x:V.in x B>in x A)>eq A B; (proof)
claim eqI:!x:V.eq x x; (proof)
claim setadjoinIL:!x:V.!y:V.in x (setadjoin x y); (proof)
claim setadjoinIR:!x:V.!A:V.!y:V.in y A>in y (setadjoin x A); (proof)
claim setadjoinE:!x:V.!A:V.!y:V.in y (setadjoin x A)>!phi:*.(eq y x>phi)>(in y A>phi)>phi; (proof)
def true:*=in emptyset (setadjoin emptyset emptyset);
claim trueI:true; (proof)
claim powersetI:!A:V.!B:V.(!x:V.in x B>in x A)>in B (powerset A); (proof)
claim powersetE:!A:V.!B:V.!x:V.in B (powerset A)>in x B>in x A; (proof)
claim setunionI:!A:V.!x:V.!B:V.in x B>in B A>in x (setunion A); (proof)
claim setunionE:!A:V.!x:V.in x (setunion A)>!phi:*.(!B:V.in x B>in B A>phi)>phi; (proof)
claim symeq:!x:V.!y:V.eq x y>eq y x; (proof)
claim transeq:!x:V.!y:V.!z:V.eq x y>eq y z>eq x z; (proof)
claim eqE2:!x:V.!y:V.!phi:V>*.eq x y>phi y>phi x; (proof)
claim symtrans1eq:!x:V.!y:V.!z:V.eq x y>eq z y>eq x z; (proof)
claim uniqinunit:!x:V.!y:V.in x (setadjoin y emptyset)>eq x y; (proof)
claim eqinunit:!x:V.!y:V.eq x y>in x (setadjoin y emptyset); (proof)
claim symtrans2eq:!x:V.!y:V.!z:V.eq x y>eq z y>eq z x; (proof)
claim boxeq:!x:V.!y:V.!z:V.!u:V.eq x y>eq z u>eq y u>eq x z; (proof)
claim dallI:!A:V.!phi:V>*.(!a:V.in a A>phi a)>dall A (\a.phi a); (proof)
claim dallE:!A:V.!phi:V>*.dall A (\a.phi a)>!a:V.in a A>phi a; (proof)
claim dexI:!A:V.!phi:V>*.!a:V.in a A>phi a>dex A (\b.phi b); (proof)
claim dexE:!A:V.!phi:V>*.dex A (\a.phi a)>!psi:*.(!a:V.in a A>phi a>psi)>psi; (proof)
claim prop2setI:!phi:*.phi>in emptyset (prop2set phi); (proof)
claim dandI:!phi:*.!psi:*.phi>psi>dand phi psi; (proof)
claim dandEL:!phi:*.!psi:*.dand phi psi>phi; (proof)
claim dandER:!phi:*.!psi:*.dand phi psi>psi; (proof)
claim dimpI:!phi:*.!psi:*.(phi>psi)>dimp phi psi; (proof)
claim dimpE:!phi:*.!psi:*.dimp phi psi>phi>psi; (proof)
claim vacuousImpI:!phi:*.!psi:*.not phi>imp phi psi; (proof)
claim trivialImpI:!phi:*.!psi:*.psi>imp phi psi; (proof)
claim excludedmiddle:!phi:*.or phi (not phi); (proof)
claim notimpE:!phi:*.!psi:*.not (imp phi psi)>and phi (not psi); (proof)
claim notimpE1:!phi:*.!psi:*.not (imp phi psi)>phi; (proof)
claim notimpE2:!phi:*.!psi:*.not (imp phi psi)>not psi; (proof)
claim notorE:!phi:*.!psi:*.not (or phi psi)>and (not phi) (not psi); (proof)
claim notorE1:!phi:*.!psi:*.not (or phi psi)>not phi; (proof)
claim notorE2:!phi:*.!psi:*.not (or phi psi)>not psi; (proof)
claim notandE:!phi:*.!psi:*.not (and phi psi)>or (not phi) (not psi); (proof)
claim notexE:!phi:V>*.not (ex (\x.phi x))>all (\x.not (phi x)); (proof)
claim notdexE:!A:V.!phi:V>*.not (dex A (\a.phi a))>dall A (\a.not (phi a)); (proof)
claim notallE:!phi:V>*.not (all (\x.phi x))>ex (\x.not (phi x)); (proof)
claim notdallE:!A:V.!phi:V>*.not (dall A (\a.phi a))>dex A (\a.not (phi a)); (proof)
claim reflequiv:!phi:*.equiv phi phi; (proof)
claim symequiv:!phi:*.!psi:*.equiv phi psi>equiv psi phi; (proof)
claim transequiv:!phi:*.!psi:*.!theta:*.equiv phi psi>equiv psi theta>equiv phi theta; (proof)
claim symtrans1equiv:!phi:*.!psi:*.!theta:*.equiv phi psi>equiv theta psi>equiv phi theta; (proof)
claim boxequiv:!phi:*.!psi:*.!theta:*.!xi:*.equiv phi psi>equiv theta xi>equiv psi xi>equiv phi theta; (proof)
claim eqCE:!phi:V>*.!x:V.phi x>!y:V.phi y>!psi:V>*.eq x y>psi x>psi y; (proof)
claim eqCE2:!phi:V>*.!x:V.phi x>!y:V.phi y>!psi:V>*.eq x y>psi y>psi x; (proof)
claim inCongP:!A:V.!B:V.eq A B>!x:V.!y:V.eq x y>in x A>in y B; (proof)
claim in__Cong:!A:V.!B:V.eq A B>!x:V.!y:V.eq x y>equiv (in x A) (in y B); (proof)
claim eqCongP:!x:V.!y:V.eq x y>!z:V.!u:V.eq z u>eq x z>eq y u; (proof)
claim eq__Cong:!x:V.!y:V.eq x y>!z:V.!u:V.eq z u>equiv (eq x z) (eq y u); (proof)
claim notCongP:!phi:*.!psi:*.equiv phi psi>not phi>not psi; (proof)
claim not__Cong:!phi:*.!psi:*.equiv phi psi>equiv (not phi) (not psi); (proof)
claim imp__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (imp phi theta) (imp psi xi); (proof)
claim equiv__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (equiv phi theta) (equiv psi xi); (proof)
claim and__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (and phi theta) (and psi xi); (proof)
claim or__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (or phi theta) (or psi xi); (proof)
claim all__Cong:!phi:V>*.!psi:V>*.(!x:V.!y:V.eq x y>equiv (phi x) (psi y))>equiv (all (\x.phi x)) (all (\x.psi x)); (proof)
claim ex__Cong:!phi:V>*.!psi:V>*.(!x:V.!y:V.eq x y>equiv (phi x) (psi y))>equiv (ex (\x.phi x)) (ex (\x.psi x)); (proof)
claim exu__Cong:!phi:V>*.!psi:V>*.(!x:V.!y:V.eq x y>equiv (phi x) (psi y))>equiv (exu (\x.phi x)) (exu (\x.psi x)); (proof)
claim emptyset__Cong:eq emptyset emptyset; (proof)
claim setadjoin__Cong:!x:V.!y:V.eq x y>!z:V.!u:V.eq z u>eq (setadjoin x z) (setadjoin y u); (proof)
claim powerset__Cong:!A:V.!B:V.eq A B>eq (powerset A) (powerset B); (proof)
claim setunion__Cong:!A:V.!B:V.eq A B>eq (setunion A) (setunion B); (proof)
claim omega__Cong:eq omega omega; (proof)
claim exuEu:!phi:V>*.exu (\x.phi x)>!x:V.!y:V.phi x>phi y>eq x y; (proof)
claim descr__Cong:!phi:V>*.!psi:V>*.(!x:V.!y:V.eq x y>equiv (phi x) (psi y))>exu (\x.phi x)>exu (\x.psi x)>eq (descr (\x.phi x)) (descr (\x.psi x)); (proof)
claim dsetconstr__Cong:!A:V.!B:V.eq A B>!phi:V>*.!psi:V>*.(!a:V.in a A>!b:V.in b B>eq a b>equiv (phi a) (psi b))>eq (dsetconstr A (\a.phi a)) (dsetconstr B (\b.psi b)); (proof)
def subset:V>V>*=\A.\B.dall A (\a.in a B);
claim subsetI1:!A:V.!B:V.(!a:V.in a A>in a B)>subset A B; (proof)
claim subsetI2:!A:V.!B:V.(!x:V.in x A>in x B)>subset A B; (proof)
claim subsetE:!A:V.!B:V.!x:V.subset A B>in x A>in x B; (proof)
claim subset2powerset:!A:V.!B:V.subset A B>in A (powerset B); (proof)
claim setextsub:!A:V.!B:V.subset A B>subset B A>eq A B; (proof)
claim powersetI1:!A:V.!B:V.subset B A>in B (powerset A); (proof)
claim powersetsubset:!A:V.!B:V.subset A B>subset (powerset A) (powerset B); (proof)
def binunion:V>V>V=\x.\y.setunion (setadjoin x (setadjoin y emptyset));
claim binunionIL:!A:V.!B:V.!x:V.in x A>in x (binunion A B); (proof)
claim upairset2IR:!x:V.!y:V.in y (setadjoin x (setadjoin y emptyset)); (proof)
claim binunionIR:!A:V.!B:V.!x:V.in x B>in x (binunion A B); (proof)
claim binunionEcases:!A:V.!B:V.!x:V.!phi:*.in x (binunion A B)>(in x A>phi)>(in x B>phi)>phi; (proof)
claim binunionE:!A:V.!B:V.!x:V.in x (binunion A B)>or (in x A) (in x B); (proof)
claim binunionLsub:!A:V.!B:V.subset A (binunion A B); (proof)
claim binunionRsub:!A:V.!B:V.subset B (binunion A B); (proof)
def binintersect:V>V>V=\A.\B.dsetconstr A (\a.in a B);
claim binintersectI:!A:V.!B:V.!x:V.in x A>in x B>in x (binintersect A B); (proof)
claim binintersectEL:!A:V.!B:V.!x:V.in x (binintersect A B)>in x A; (proof)
claim binintersectER:!A:V.!B:V.!x:V.in x (binintersect A B)>in x B; (proof)
def setminus:V>V>V=\A.\B.dsetconstr A (\a.not (in a B));
def iskpair:V>*=\A.dex (setunion A) (\x.dex (setunion A) (\y.eq A (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset))));
claim secondinupair:!x:V.!y:V.in y (setadjoin x (setadjoin y emptyset)); (proof)
claim setukpairIL:!x:V.!y:V.in x (setunion (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset))); (proof)
claim setukpairIR:!x:V.!y:V.in y (setunion (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset))); (proof)
claim kpairiskpair:!x:V.!y:V.iskpair (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)); (proof)
def kpair:V>V>V=\x.\y.setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset);
claim kpairp:!x:V.!y:V.iskpair (kpair x y); (proof)
def cartprod:V>V>V=\A.\B.dsetconstr (powerset (powerset (binunion A B))) (\x.dex A (\a.dex B (\b.eq x (kpair a b))));
claim singletonsubset:!A:V.!a:V.in a A>subset (setadjoin a emptyset) A; (proof)
claim singletoninpowerset:!A:V.!a:V.in a A>in (setadjoin a emptyset) (powerset A); (proof)
claim singletoninpowunion:!A:V.!B:V.!a:V.in a A>in (setadjoin a emptyset) (powerset (binunion A B)); (proof)
claim upairset2E:!x:V.!y:V.!z:V.in z (setadjoin x (setadjoin y emptyset))>or (eq z x) (eq z y); (proof)
claim upairsubunion:!A:V.!B:V.!a:V.in a A>!b:V.in b B>subset (setadjoin a (setadjoin b emptyset)) (binunion A B); (proof)
claim upairinpowunion:!A:V.!B:V.!a:V.in a A>!b:V.in b B>in (setadjoin a (setadjoin b emptyset)) (powerset (binunion A B)); (proof)
claim ubforcartprodlem1:!A:V.!B:V.!a:V.in a A>!b:V.in b B>subset (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin b emptyset)) emptyset)) (powerset (binunion A B)); (proof)
claim ubforcartprodlem2:!A:V.!B:V.!a:V.in a A>!b:V.in b B>in (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin b emptyset)) emptyset)) (powerset (powerset (binunion A B))); (proof)
claim ubforcartprodlem3:!A:V.!B:V.!a:V.in a A>!b:V.in b B>in (kpair a b) (powerset (powerset (binunion A B))); (proof)
claim cartprodpairin:!A:V.!B:V.!a:V.in a A>!b:V.in b B>in (kpair a b) (cartprod A B); (proof)
claim cartprodmempair1:!A:V.!B:V.!u:V.in u (cartprod A B)>dex A (\a.dex B (\b.eq u (kpair a b))); (proof)
claim cartprodmempair:!A:V.!B:V.!u:V.in u (cartprod A B)>iskpair u; (proof)
claim setunionE2:!A:V.!x:V.in x (setunion A)>dex A (\a.in x a); (proof)
claim setunionsingleton1:!A:V.subset (setunion (setadjoin A emptyset)) A; (proof)
claim setunionsingleton2:!A:V.subset A (setunion (setadjoin A emptyset)); (proof)
claim setunionsingleton:!x:V.eq (setunion (setadjoin x emptyset)) x; (proof)
def singleton:V>*=\A.dex A (\a.eq A (setadjoin a emptyset));
def ex1:V>(V>*)>*=\A.\phi.singleton (dsetconstr A (\a.phi a));
claim ex1I:!A:V.!phi:V>*.!a:V.in a A>phi a>(!b:V.in b A>phi b>eq b a)>ex1 A (\b.phi b); (proof)
claim singletonsuniq:!x:V.!y:V.eq (setadjoin x emptyset) (setadjoin y emptyset)>eq x y; (proof)
claim setukpairinjL1:!x:V.!y:V.!z:V.in (setadjoin z emptyset) (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset))>eq x z; (proof)
claim kfstsingleton:!u:V.iskpair u>singleton (dsetconstr (setunion u) (\x.in (setadjoin x emptyset) u)); (proof)
claim theprop:!X:V.singleton X>in (setunion X) X; (proof)
def kfst:V>V=\u.setunion (dsetconstr (setunion u) (\x.in (setadjoin x emptyset) u));
claim kfstpairEq:!x:V.!y:V.eq (kfst (kpair x y)) x; (proof)
claim cartprodfstin:!A:V.!B:V.!u:V.in u (cartprod A B)>in (kfst u) A; (proof)
claim setukpairinjL2:!x:V.!y:V.!z:V.!u:V.eq (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)) (setadjoin (setadjoin z emptyset) (setadjoin (setadjoin z (setadjoin u emptyset)) emptyset))>eq x z; (proof)
claim setukpairinjR11:!x:V.!y:V.eq x y>eq (setadjoin x (setadjoin y emptyset)) (setadjoin x emptyset); (proof)
claim setukpairinjR12:!x:V.!y:V.eq x y>eq (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)) (setadjoin (setadjoin x emptyset) emptyset); (proof)
claim setukpairinjR1:!x:V.!y:V.!z:V.!u:V.eq (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)) (setadjoin (setadjoin z emptyset) (setadjoin (setadjoin z (setadjoin u emptyset)) emptyset))>eq z u>eq y u; (proof)
claim upairequniteq:!x:V.!y:V.!z:V.eq (setadjoin x (setadjoin y emptyset)) (setadjoin z emptyset)>eq x y; (proof)
claim setukpairinjR2:!x:V.!y:V.!z:V.!u:V.eq (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)) (setadjoin (setadjoin z emptyset) (setadjoin (setadjoin z (setadjoin u emptyset)) emptyset))>eq y u; (proof)
claim setukpairinjR:!x:V.!y:V.!z:V.!u:V.eq (kpair x y) (kpair z u)>eq y u; (proof)
claim ksndsingleton:!u:V.iskpair u>singleton (dsetconstr (setunion u) (\x.eq u (kpair (kfst u) x))); (proof)
def ksnd:V>V=\u.setunion (dsetconstr (setunion u) (\x.eq u (kpair (kfst u) x)));
claim ksndpairEq:!x:V.!y:V.eq (ksnd (kpair x y)) y; (proof)
claim cartprodsndin:!A:V.!B:V.!u:V.in u (cartprod A B)>in (ksnd u) B; (proof)
claim cartprodmempaircEq:!A:V.!B:V.!a:V.in a A>!b:V.in b B>eq (kpair a b) (kpair a b); (proof)
claim cartprodfstpairEq:!A:V.!B:V.!a:V.in a A>!b:V.in b B>eq (kfst (kpair a b)) a; (proof)
claim cartprodsndpairEq:!A:V.!B:V.!a:V.in a A>!b:V.in b B>eq (ksnd (kpair a b)) b; (proof)
claim cartprodpairsurjEq:!A:V.!B:V.!u:V.in u (cartprod A B)>eq (kpair (kfst u) (ksnd u)) u; (proof)
def breln:V>V>V>*=\A.\B.\C.subset C (cartprod A B);
def dpsetconstr:V>V>(V>V>*)>V=\A.\B.\phi.dsetconstr (cartprod A B) (\u.dex A (\a.dex B (\b.and (phi a b) (eq u (kpair a b)))));
def func:V>V>V>*=\A.\B.\R.and (breln A B R) (dall A (\a.ex1 B (\b.in (kpair a b) R)));
def funcSet:V>V>V=\A.\B.dsetconstr (powerset (cartprod A B)) (\f.func A B f);
claim funcImageSingleton:!A:V.!B:V.!f:V.func A B f>!a:V.in a A>singleton (dsetconstr B (\b.in (kpair a b) f)); (proof)
claim apProp:!A:V.!B:V.!f:V.func A B f>!a:V.in a A>in (setunion (dsetconstr B (\b.in (kpair a b) f))) B; (proof)
def ap:V>V>V>V>V=\A.\B.\f.\a.setunion (dsetconstr B (\b.in (kpair a b) f));
claim app:!A:V.!B:V.!f:V.func A B f>!a:V.in a A>in (ap A B f a) B; (proof)
claim infuncsetfunc:!A:V.!B:V.!f:V.in f (funcSet A B)>func A B f; (proof)
claim ap2p:!A:V.!B:V.!f:V.in f (funcSet A B)>!a:V.in a A>in (ap A B f a) B; (proof)
claim dpsetconstrI:!A:V.!B:V.!phi:V>V>*.!a:V.in a A>!b:V.in b B>phi a b>in (kpair a b) (dpsetconstr A B (\x.\c.phi x c)); (proof)
claim dpsetconstrSub:!A:V.!B:V.!phi:V>V>*.subset (dpsetconstr A B (\a.\b.phi a b)) (cartprod A B); (proof)
claim funcinfuncset:!A:V.!B:V.!f:V.func A B f>in f (funcSet A B); (proof)
claim setOfPairsIsBReln:!A:V.!B:V.!phi:V>V>*.breln A B (dpsetconstr A B (\a.\b.phi a b)); (proof)
claim setukpairinjL:!x:V.!y:V.!z:V.!u:V.eq (kpair x y) (kpair z u)>eq x z; (proof)
claim dpsetconstrERa:!A:V.!B:V.!phi:V>V>*.!a:V.in a A>!b:V.in b B>in (kpair a b) (dpsetconstr A B (\x.\c.phi x c))>phi a b; (proof)
claim lamProp:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>func A B (dpsetconstr A B (\a.\b.eq (f a) b)); (proof)
def lam:V>V>(V>V)>V=\A.\B.\f.dpsetconstr A B (\a.\b.eq (f a) b);
claim lamp:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>func A B (lam A B (\a.f a)); (proof)
claim lam2p:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>in (lam A B (\a.f a)) (funcSet A B); (proof)
claim brelnall1:!A:V.!B:V.!R:V.breln A B R>!phi:V>*.(!a:V.in a A>!b:V.in b B>in (kpair a b) R>phi (kpair a b))>dall R (\x.phi x); (proof)
claim ex1E2:!A:V.!phi:V>*.ex1 A (\a.phi a)>!a:V.in a A>!b:V.in b A>phi a>phi b>eq a b; (proof)
claim funcGraphProp1:!A:V.!B:V.!f:V.func A B f>!a:V.in a A>in (kpair a (ap A B f a)) f; (proof)
claim funcGraphProp2:!A:V.!B:V.!f:V.func A B f>!a:V.in a A>!b:V.in b B>in (kpair a b) f>eq (ap A B f a) b; (proof)
claim subbreln:!A:V.!B:V.!R:V.breln A B R>!S:V.breln A B S>(!a:V.in a A>!b:V.in b B>in (kpair a b) R>in (kpair a b) S)>subset R S; (proof)
claim eqbreln:!A:V.!B:V.!R:V.breln A B R>!S:V.breln A B S>(!a:V.in a A>!b:V.in b B>in (kpair a b) R>in (kpair a b) S)>(!a:V.in a A>!b:V.in b B>in (kpair a b) S>in (kpair a b) R)>eq R S; (proof)
claim funcext:!A:V.!B:V.!f:V.func A B f>!g:V.func A B g>(!a:V.in a A>eq (ap A B f a) (ap A B g a))>eq f g; (proof)
claim funcext2:!A:V.!B:V.!f:V.in f (funcSet A B)>!g:V.in g (funcSet A B)>(!a:V.in a A>eq (ap A B f a) (ap A B g a))>eq f g; (proof)
claim ap2apEq1:!A:V.!B:V.!f:V.in f (funcSet A B)>!a:V.in a A>eq (ap A B f a) (ap A B f a); (proof)
claim beta1:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>!a:V.in a A>eq (ap A B (lam A B (\x.f x)) a) (f a); (proof)
claim lam2lamEq:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>eq (lam A B (\a.f a)) (lam A B (\a.f a)); (proof)
claim beta2:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>!a:V.in a A>eq (ap A B (lam A B (\x.f x)) a) (f a); (proof)
claim eta2:!A:V.!B:V.!f:V.in f (funcSet A B)>eq (lam A B (\a.ap A B f a)) f; (proof)
claim iffalseProp1:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>not phi>in b (dsetconstr A (\c.or (and phi (eq c a)) (and (not phi) (eq c b)))); (proof)
claim iffalseProp2:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>not phi>eq (dsetconstr A (\c.or (and phi (eq c a)) (and (not phi) (eq c b)))) (setadjoin b emptyset); (proof)
claim iftrueProp1:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>phi>in a (dsetconstr A (\c.or (and phi (eq c a)) (and (not phi) (eq c b)))); (proof)
claim iftrueProp2:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>phi>eq (dsetconstr A (\c.or (and phi (eq c a)) (and (not phi) (eq c b)))) (setadjoin a emptyset); (proof)
claim ifSingleton:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>singleton (dsetconstr A (\c.or (and phi (eq c a)) (and (not phi) (eq c b)))); (proof)
claim powersetE1:!A:V.!B:V.in B (powerset A)>subset B A; (proof)
claim sepInPowerset:!A:V.!phi:V>*.in (dsetconstr A (\a.phi a)) (powerset A); (proof)
claim sepSubset:!A:V.!phi:V>*.subset (dsetconstr A (\a.phi a)) A; (proof)
def if:V>*>V>V>V=\A.\phi.\a.\b.setunion (dsetconstr A (\c.or (and phi (eq c a)) (and (not phi) (eq c b))));
claim ifp:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>in (if A phi a b) A; (proof)
claim theeq:!X:V.singleton X>!x:V.in x X>eq (setunion X) x; (proof)
claim iftrue:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>phi>eq (if A phi a b) a; (proof)
claim iffalse:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>not phi>eq (if A phi a b) b; (proof)
claim iftrueorfalse:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>in (if A phi a b) (setadjoin a (setadjoin b emptyset)); (proof)
claim bs114d:!A:V.!B:V.!C:V.eq (binintersect A (binunion B C)) (binunion (binintersect A B) (binintersect A C)); (proof)
claim binintersectT_lem:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (binintersect X Y) (powerset A); (proof)
claim binunionT_lem:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (binunion X Y) (powerset A); (proof)
claim powersetT_lem:!A:V.!X:V.in X (powerset A)>in (powerset X) (powerset (powerset A)); (proof)
claim setminusEL:!A:V.!B:V.!x:V.in x (setminus A B)>in x A; (proof)
claim setminusT_lem:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (setminus X Y) (powerset A); (proof)
claim complementT_lem:!A:V.!X:V.in X (powerset A)>in (setminus A X) (powerset A); (proof)
claim setextT:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>(!a:V.in a A>in a X>in a Y)>(!a:V.in a A>in a Y>in a X)>eq X Y; (proof)
claim subsetTI:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>(!a:V.in a A>in a X>in a Y)>subset X Y; (proof)
claim powersetTI1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>(!a:V.in a A>in a X>in a Y)>in X (powerset Y); (proof)
claim powersetTE1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in X (powerset Y)>in a X>in a Y; (proof)
claim setminusI:!A:V.!B:V.!x:V.in x A>not (in x B)>in x (setminus A B); (proof)
claim setminusER:!A:V.!B:V.!x:V.in x (setminus A B)>not (in x B); (proof)
claim complementTI1:!A:V.!X:V.in X (powerset A)>!a:V.in a A>in a X>not (in a (setminus A X)); (proof)
claim complementTE1:!A:V.!X:V.in X (powerset A)>!a:V.in a A>not (in a (setminus A X))>in a X; (proof)
claim binintersectTELcontra:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>not (in a X)>not (in a (binintersect X Y)); (proof)
claim binintersectTERcontra:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>not (in a Y)>not (in a (binintersect X Y)); (proof)
claim contrasubsetT:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>subset X (setminus A Y)>in a Y>not (in a X); (proof)
claim contrasubsetT1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>subset X Y>not (in a Y)>not (in a X); (proof)
claim contrasubsetT2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>subset X Y>subset (setminus A Y) (setminus A X); (proof)
claim contrasubsetT3:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>subset (setminus A Y) (setminus A X)>subset X Y; (proof)
claim doubleComplementI1:!A:V.!X:V.in X (powerset A)>!a:V.in a A>in a X>in a (setminus A (setminus A X)); (proof)
claim doubleComplementE1:!A:V.!X:V.in X (powerset A)>!a:V.in a A>in a (setminus A (setminus A X))>in a X; (proof)
claim doubleComplementSub1:!A:V.!X:V.in X (powerset A)>subset X (setminus A (setminus A X)); (proof)
claim doubleComplementSub2:!A:V.!X:V.in X (powerset A)>subset (setminus A (setminus A X)) X; (proof)
claim doubleComplementEq:!A:V.!X:V.in X (powerset A)>eq X (setminus A (setminus A X)); (proof)
claim binintersectLsub:!A:V.!B:V.subset (binintersect A B) A; (proof)
claim binintersectRsub:!A:V.!B:V.subset (binintersect A B) B; (proof)
claim complementTnotintersectT:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A X)>not (in a (binintersect X Y)); (proof)
claim complementImpComplementIntersect:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A X)>in a (setminus A (binintersect X Y)); (proof)
claim complementSubsetComplementIntersect:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>subset (setminus A X) (setminus A (binintersect X Y)); (proof)
claim complementInPowersetComplementIntersect:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (setminus A X) (powerset (setminus A (binintersect X Y))); (proof)
claim contraSubsetComplement:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>subset X (setminus A Y)>!a:V.in a A>in a Y>in a (setminus A X); (proof)
claim complementTcontraSubset:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>subset X (setminus A Y)>subset Y (setminus A X); (proof)
claim binunionTILcontra:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>not (in a (binunion X Y))>not (in a X); (proof)
claim binunionTIRcontra:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>not (in a (binunion X Y))>not (in a Y); (proof)
claim inIntersectImpInUnion:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>!a:V.in a A>in a (binintersect X Y)>in a (binunion X Z); (proof)
claim inIntersectImpInUnion2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>!a:V.in a A>in a (binintersect X Y)>in a (binunion Y Z); (proof)
claim inIntersectImpInIntersectUnions:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>!a:V.in a A>in a (binintersect X Y)>in a (binintersect (binunion X Z) (binunion Y Z)); (proof)
claim intersectInPowersetIntersectUnions:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>in (binintersect X Y) (powerset (binintersect (binunion X Z) (binunion Y Z))); (proof)
claim inComplementUnionImpNotIn1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A (binunion X Y))>not (in a X); (proof)
claim inComplementUnionImpInComplement1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A (binunion X Y))>in a (setminus A X); (proof)
claim binunionTE:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!phi:*.!a:V.in a A>in a (binunion X Y)>(in a X>phi)>(in a Y>phi)>phi; (proof)
claim binunionTEcontra:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>not (in a X)>not (in a Y)>not (in a (binunion X Y)); (proof)
claim demorgan2a1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A (binunion X Y))>in a (setminus A X); (proof)
claim demorgan2a2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A (binunion X Y))>in a (setminus A Y); (proof)
claim demorgan1a:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A (binintersect X Y))>in a (binunion (setminus A X) (setminus A Y)); (proof)
claim demorgan1b:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (binunion (setminus A X) (setminus A Y))>in a (setminus A (binintersect X Y)); (proof)
claim demorgan1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>eq (setminus A (binintersect X Y)) (binunion (setminus A X) (setminus A Y)); (proof)
claim demorgan2a:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A (binunion X Y))>in a (binintersect (setminus A X) (setminus A Y)); (proof)
claim demorgan2b2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (setminus A X)>in a (setminus A Y)>in a (setminus A (binunion X Y)); (proof)
claim demorgan2b:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!a:V.in a A>in a (binintersect (setminus A X) (setminus A Y))>in a (setminus A (binunion X Y)); (proof)
claim demorgan2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>eq (setminus A (binunion X Y)) (binintersect (setminus A X) (setminus A Y)); (proof)
claim woz13rule0:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!x:V.in x (binintersect X Y)>in x A; (proof)
claim woz13rule1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>subset X Z>subset (binintersect X Y) Z; (proof)
claim woz13rule2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>subset Y Z>subset (binintersect X Y) Z; (proof)
claim woz13rule3:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>subset X Y>subset X Z>subset X (binintersect Y Z); (proof)
claim woz13rule4:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>!W:V.in W (powerset A)>subset X Z>subset Y W>subset (binintersect X Y) (binintersect Z W); (proof)
claim woz1_1:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (setminus A X) (powerset (setminus A (binintersect X Y))); (proof)
claim woz1_2:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>!W:V.in W (powerset A)>eq (setminus A (binintersect (binunion X Y) (binunion Z W))) (binunion (binintersect (setminus A X) (setminus A Y)) (binintersect (setminus A Z) (setminus A W))); (proof)
claim woz1_3:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>!Z:V.in Z (powerset A)>in (binintersect X Y) (powerset (binintersect (binunion X Z) (binunion Y Z))); (proof)
claim woz1_4:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>subset X (setminus A Y)>subset Y (setminus A X); (proof)
claim woz1_5:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (setminus A (binunion X Y)) (powerset (setminus A X)); (proof)
def breln1:V>V>*=\A.\R.breln A A R;
claim breln1all1:!A:V.!R:V.breln1 A R>!phi:V>*.(!a:V.in a A>!b:V.in b A>in (kpair a b) R>phi (kpair a b))>dall R (\x.phi x); (proof)
claim subbreln1:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>(!a:V.in a A>!b:V.in b A>in (kpair a b) R>in (kpair a b) S)>subset R S; (proof)
claim eqbreln1:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>(!a:V.in a A>!b:V.in b A>in (kpair a b) R>in (kpair a b) S)>(!a:V.in a A>!b:V.in b A>in (kpair a b) S>in (kpair a b) R)>eq R S; (proof)
def breln1invset:V>V>V=\A.\R.dpsetconstr A A (\a.\b.in (kpair b a) R);
claim setOfPairsIsBReln1:!A:V.!phi:V>V>*.breln1 A (dpsetconstr A A (\a.\b.phi a b)); (proof)
claim breln1invprop:!A:V.!R:V.breln1 A R>breln1 A (breln1invset A R); (proof)
claim breln1invI:!A:V.!R:V.breln1 A R>!a:V.in a A>!b:V.in b A>in (kpair a b) R>in (kpair b a) (breln1invset A R); (proof)
claim cartprodpairmemEL:!A:V.!B:V.!x:V.!y:V.in (kpair x y) (cartprod A B)>in x A; (proof)
claim cartprodpairmemER:!A:V.!B:V.!x:V.!y:V.in (kpair x y) (cartprod A B)>in y B; (proof)
claim dpsetconstrEL1:!A:V.!B:V.!phi:V>V>*.!x:V.!y:V.in (kpair x y) (dpsetconstr A B (\a.\b.phi a b))>in x A; (proof)
claim dpsetconstrEL2:!A:V.!B:V.!phi:V>V>*.!x:V.!y:V.in (kpair x y) (dpsetconstr A B (\a.\b.phi a b))>in y B; (proof)
claim dpsetconstrER:!A:V.!B:V.!phi:V>V>*.!x:V.!y:V.in (kpair x y) (dpsetconstr A B (\a.\b.phi a b))>phi x y; (proof)
claim breln1invE:!A:V.!R:V.breln1 A R>!a:V.in a A>!b:V.in b A>in (kpair b a) (breln1invset A R)>in (kpair a b) R; (proof)
def breln1compset:V>V>V>V=\A.\R.\S.dpsetconstr A A (\a.\b.dex A (\c.and (in (kpair a c) R) (in (kpair c b) S)));
claim breln1compprop:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>breln1 A (breln1compset A R S); (proof)
claim breln1compI:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>!c:V.in c A>in (kpair a c) R>in (kpair c b) S>in (kpair a b) (breln1compset A R S); (proof)
claim breln1compE:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>in (kpair a b) (breln1compset A R S)>dex A (\c.and (in (kpair a c) R) (in (kpair c b) S)); (proof)
claim breln1unionprop:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>breln1 A (binunion R S); (proof)
claim breln1unionIL:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>in (kpair a b) R>in (kpair a b) (binunion R S); (proof)
claim breln1unionIR:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>in (kpair a b) S>in (kpair a b) (binunion R S); (proof)
claim breln1unionI:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>or (in (kpair a b) R) (in (kpair a b) S)>in (kpair a b) (binunion R S); (proof)
claim breln1unionE:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>in (kpair a b) (binunion R S)>or (in (kpair a b) R) (in (kpair a b) S); (proof)
claim breln1unionEcases:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>in (kpair a b) (binunion R S)>!phi:*.(in (kpair a b) R>phi)>(in (kpair a b) S>phi)>phi; (proof)
claim breln1unionCommutes:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>eq (binunion R S) (binunion S R); (proof)
claim woz2Ex:!A:V.!R:V.breln1 A R>eq R (breln1invset A (breln1invset A R)); (proof)
claim woz2W:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>eq (breln1invset A (breln1compset A R S)) (breln1compset A (breln1invset A S) (breln1invset A R)); (proof)
claim woz2A:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!T:V.breln1 A T>eq (breln1compset A (binunion R S) T) (binunion (breln1compset A R T) (breln1compset A S T)); (proof)
claim woz2B:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!T:V.breln1 A T>eq (breln1compset A (binunion R S) T) (binunion (breln1invset A (breln1compset A (breln1invset A T) (breln1invset A S))) (breln1invset A (breln1compset A (breln1invset A T) (breln1invset A R)))); (proof)
claim ap2apEq2:!A:V.!B:V.!f:V.func A B f>!a:V.in a A>eq (ap A B f a) (ap A B f a); (proof)
def atleast2p:V>*=\A.dex A (\a.dex A (\b.not (eq a b)));
def atmost1p:V>*=\A.dall A (\a.dall A (\b.eq a b));
def atmost2p:V>*=\A.dall A (\a.dall A (\b.dall A (\c.or (eq a c) (eq b c))));
claim binintersectSubset1:!A:V.!B:V.eq (binintersect A B) A>subset A B; (proof)
claim binintersectSubset2:!A:V.!B:V.subset A B>eq (binintersect A B) A; (proof)
claim binintersectSubset3:!A:V.!B:V.eq (binintersect A B) B>subset B A; (proof)
claim binintersectSubset4:!A:V.!B:V.subset B A>eq (binintersect A B) B; (proof)
claim binintersectSubset5:!A:V.!B:V.!C:V.subset C A>subset C B>subset C (binintersect A B); (proof)
claim boolDeMorgan1:!phi:*.!psi:*.not (and phi psi)>or (not phi) (not psi); (proof)
claim boolDeMorgan2:!phi:*.!psi:*.or (not phi) (not psi)>not (and phi psi); (proof)
claim boolDeMorgan3:!phi:*.!psi:*.not (or phi psi)>and (not phi) (not psi); (proof)
claim boolDeMorgan3a:!phi:*.!psi:*.not (imp phi psi)>and phi (not psi); (proof)
claim boolDeMorgan4:!phi:*.!psi:*.and (not phi) (not psi)>not (or phi psi); (proof)
claim boolDeMorgan4a:!phi:*.!psi:*.and phi (not psi)>not (imp phi psi); (proof)
def breln1Set:V>V=\A.dsetconstr (powerset (cartprod A A)) (\R.breln1 A R);
def antisymmetric:V>V>*=\A.\R.dall A (\a.dall A (\b.imp (and (in (kpair a b) R) (in (kpair b a) R)) (eq a b)));
claim breln1SetBreln1:!A:V.!R:V.in R (breln1Set A)>breln1 A R; (proof)
claim breln1compEex:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>!a:V.in a A>!b:V.in b A>in (kpair a b) (breln1compset A R S)>!phi:*.(!c:V.in c A>in (kpair a c) R>in (kpair c b) S>phi)>phi; (proof)
claim brelnall2:!A:V.!B:V.!R:V.breln A B R>!phi:V>*.dall A (\a.dall B (\b.imp (in (kpair a b) R) (phi (kpair a b))))>dall R (\x.phi x); (proof)
claim breln1all2:!A:V.!R:V.breln1 A R>!phi:V>*.dall A (\a.dall A (\b.imp (in (kpair a b) R) (phi (kpair a b))))>dall R (\x.phi x); (proof)
claim complementUnionInPowersetComplement:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (setminus A (binunion X Y)) (powerset (setminus A X)); (proof)
claim contrapositive1a:!phi:*.!psi:*.imp phi psi>not psi>not phi; (proof)
claim contrapositive2a:!phi:*.!psi:*.imp (not phi) psi>not psi>phi; (proof)
claim contrapositive3a:!phi:*.!psi:*.imp (not phi) (not psi)>psi>phi; (proof)
claim contrapositive4a:!phi:*.!psi:*.imp phi (not psi)>psi>not phi; (proof)
def disjoint:V>V>*=\A.\B.not (dex A (\a.in a B));
claim emptyE1:!A:V.!phi:V>*.dex A (\a.phi a)>eq (dsetconstr A (\a.phi a)) emptyset>false; (proof)
claim emptyI:!A:V.(!x:V.not (in x A))>eq A emptyset; (proof)
claim disjointsetsI1:!A:V.!B:V.not (ex (\x.and (in x A) (in x B)))>eq (binintersect A B) emptyset; (proof)
claim emptyInPowerset:!A:V.in emptyset (powerset A); (proof)
claim emptyinPowerset:!A:V.in emptyset (powerset A); (proof)
claim emptyinunitempty:in emptyset (setadjoin emptyset emptyset); (proof)
claim emptysetimpfalse:!x:V.in x emptyset>false; (proof)
claim emptysetsubset:!A:V.subset emptyset A; (proof)
claim eqET:!A:V.!a:V.in a A>!b:V.in b A>eq a b>!phi:V>*.phi a>phi b; (proof)
claim eqET2:!A:V.!a:V.in a A>!b:V.in b A>eq a b>!phi:V>*.phi b>phi a; (proof)
claim eqimpsubset1:!A:V.!B:V.eq A B>subset A B; (proof)
claim eqimpsubset2:!A:V.!B:V.eq A B>subset B A; (proof)
claim equivAndE1:!phi:*.!psi:*.!theta:*.equiv phi (and psi theta)>phi>psi; (proof)
claim equivAndE2:!phi:*.!psi:*.!theta:*.equiv phi (and psi theta)>phi>theta; (proof)
claim equivAndE3:!phi:*.!psi:*.!theta:*.equiv phi (and psi theta)>psi>theta>phi; (proof)
claim equivOrE1:!phi:*.!psi:*.!theta:*.equiv phi (or psi theta)>psi>phi; (proof)
claim equivOrE2:!phi:*.!psi:*.!theta:*.equiv phi (or psi theta)>theta>phi; (proof)
claim eta1:!A:V.!B:V.!f:V.func A B f>eq (lam A B (\a.ap A B f a)) f; (proof)
claim ex1E1:!A:V.!phi:V>*.ex1 A (\a.phi a)>dex A (\a.phi a); (proof)
claim exuE1:!phi:V>*.exu (\x.phi x)>ex (\x.and (phi x) (all (\y.imp (phi y) (eq x y)))); (proof)
claim exuE2:!phi:V>*.exu (\x.phi x)>ex (\x.all (\y.equiv (phi y) (eq y x))); (proof)
claim exuE3e:!phi:V>*.exu (\x.phi x)>ex (\x.phi x); (proof)
claim exuE3u:!phi:V>*.exu (\x.phi x)>!x:V.!y:V.phi x>phi y>eq x y; (proof)
claim exuI1:!phi:V>*.ex (\x.and (phi x) (all (\y.imp (phi y) (eq x y))))>exu (\x.phi x); (proof)
claim exuI2:!phi:V>*.ex (\x.all (\y.equiv (phi y) (eq y x)))>exu (\x.phi x); (proof)
claim exuI3:!phi:V>*.ex (\x.phi x)>all (\x.all (\y.imp (phi x) (imp (phi y) (eq x y))))>exu (\x.phi x); (proof)
claim emptynotinempty:not (in emptyset emptyset); (proof)
claim funcGraphProp3:!A:V.!B:V.!f:V.in f (funcSet A B)>!a:V.in a A>in (kpair a (ap A B f a)) f; (proof)
claim funcGraphProp4:!A:V.!B:V.!f:V.in f (funcSet A B)>!a:V.in a A>!b:V.in b B>in (kpair a b) f>eq (ap A B f a) b; (proof)
claim funcextLem:!A:V.!B:V.!f:V.func A B f>!g:V.func A B g>(!a:V.in a A>eq (ap A B f a) (ap A B g a))>!a:V.in a A>!b:V.in b B>in (kpair a b) g>in (kpair a b) f; (proof)
claim image1Ex:!A:V.!f:V>V.ex (\B.all (\x.equiv (in x B) (dex A (\a.eq x (f a))))); (proof)
claim image1Ex1:!A:V.!f:V>V.exu (\B.all (\x.equiv (in x B) (dex A (\a.eq x (f a))))); (proof)
def image1:V>(V>V)>V=\A.\f.descr (\B.all (\x.equiv (in x B) (dex A (\a.eq x (f a)))));
claim image1Equiv:!A:V.!f:V>V.!x:V.equiv (in x (image1 A (\a.f a))) (dex A (\a.eq x (f a))); (proof)
claim image1E:!A:V.!f:V>V.!x:V.in x (image1 A (\a.f a))>dex A (\a.eq x (f a)); (proof)
claim image1I:!A:V.!f:V>V.!x:V.dex A (\a.eq x (f a))>in x (image1 A (\a.f a)); (proof)
def injective:V>V>V>*=\A.\B.\f.dall A (\a.dall A (\b.imp (eq (ap A B f a) (ap A B f b)) (eq a b)));
def injFuncSet:V>V>V=\A.\B.dsetconstr (funcSet A B) (\f.injective A B f);
claim injFuncInInjFuncSet:!A:V.!B:V.!f:V.in f (funcSet A B)>injective A B f>in f (injFuncSet A B); (proof)
claim injFuncSetFuncIn:!A:V.!B:V.!f:V.in f (injFuncSet A B)>in f (funcSet A B); (proof)
claim injFuncSetFuncInj:!x:V.!y:V.!f:V.in f (injFuncSet x y)>injective x y f; (proof)
claim kpairsurjEq:!u:V.iskpair u>eq (kpair (kfst u) (ksnd u)) u; (proof)
def nonempty:V>*=\x.not (eq x emptyset);
claim nonemptyE1:!A:V.nonempty A>ex (\x.in x A); (proof)
claim foundation2:!A:V.imp (nonempty A) (dex A (\a.eq (binintersect a A) emptyset)); (proof)
claim nonemptyI:!A:V.!phi:V>*.!a:V.in a A>phi a>nonempty (dsetconstr A (\b.phi b)); (proof)
claim nonemptyI1:!A:V.ex (\x.in x A)>nonempty A; (proof)
claim notequalI1:!A:V.!B:V.not (subset A B)>not (eq A B); (proof)
claim notfalse:not false; (proof)
claim notinemptyset:!x:V.not (in x emptyset); (proof)
claim notinself:!A:V.not (in A A); (proof)
claim notinself2:!A:V.!B:V.in A B>not (in B A); (proof)
claim notinsingleton:!x:V.!y:V.not (eq x y)>not (in y (setadjoin x emptyset)); (proof)
claim notsubsetI:!A:V.!B:V.!x:V.in x A>not (in x B)>not (subset A B); (proof)
claim notequalI2:!A:V.!B:V.!x:V.in x A>not (in x B)>not (eq A B); (proof)
def omegaS:V>V=\x.setadjoin x x;
claim omegaSp:!x:V.in x omega>in (omegaS x) omega; (proof)
claim omegaSclos:!x:V.in x omega>in (setadjoin x x) omega; (proof)
claim peano0notS:!x:V.in x omega>not (eq (omegaS x) emptyset); (proof)
def peano3:V>V>V>*=\A.\a.\f.dall A (\b.not (eq (ap A A f b) a));
def peano4:V>V>V>*=\A.\a.\f.dall A (\b.dall A (\c.imp (eq (ap A A f b) (ap A A f c)) (eq b c)));
def peano5:V>V>V>*=\A.\a.\f.dall (powerset A) (\X.imp (and (in a X) (dall A (\b.imp (in b X) (in (ap A A f b) X)))) (eq X A));
claim peanoSinj:!x:V.in x omega>!y:V.in y omega>eq (omegaS x) (omegaS y)>eq x y; (proof)
def peano:V>V>V>*=\A.\x.\f.dand (in x A) (dand (in f (funcSet A A)) (and (and (peano3 A x f) (peano4 A x f)) (peano5 A x f)));
claim quantDeMorgan1:!A:V.!phi:V>*.not (dall A (\a.phi a))>dex A (\a.not (phi a)); (proof)
claim quantDeMorgan2:!A:V.!phi:V>*.dall A (\a.not (phi a))>not (dex A (\a.phi a)); (proof)
claim quantDeMorgan3:!A:V.!phi:V>*.not (dex A (\a.phi a))>dall A (\a.not (phi a)); (proof)
claim quantDeMorgan4:!A:V.!phi:V>*.dex A (\a.not (phi a))>not (dall A (\a.phi a)); (proof)
def reflexive:V>V>*=\A.\R.dall A (\a.in (kpair a a) R);
def regular:V>*=\A.dex A (\a.eq (binintersect a A) emptyset);
def set2prop:V>*=\A.in emptyset A;
claim prop2set2propI:!phi:*.phi>set2prop (prop2set phi); (proof)
claim setadjoinOr:!x:V.!A:V.!y:V.in y (setadjoin x A)>or (eq y x) (in y A); (proof)
claim setadjoinSub:!x:V.!A:V.subset A (setadjoin x A); (proof)
claim setbeta:!A:V.!phi:V>*.!a:V.in a A>equiv (in a (dsetconstr A (\b.phi b))) (phi a); (proof)
claim setminusERneg:!A:V.!B:V.!x:V.not (in x (setminus A B))>in x A>in x B; (proof)
claim setminusELneg:!A:V.!B:V.!x:V.not (in x (setminus A B))>not (in x B)>not (in x A); (proof)
claim setminusILneg:!A:V.!B:V.!x:V.not (in x A)>not (in x (setminus A B)); (proof)
claim setminusIRneg:!A:V.!B:V.!x:V.in x B>not (in x (setminus A B)); (proof)
claim setminusLsub:!A:V.!B:V.subset (setminus A B) A; (proof)
claim setminusSubset1:!A:V.!B:V.eq (setminus A B) emptyset>subset A B; (proof)
claim setoftrueEq:!A:V.eq (dsetconstr A (\a.true)) A; (proof)
claim nonemptyImpWitness:!A:V.nonempty A>dex A (\a.true); (proof)
def setsmeet:V>V>*=\A.\B.dex A (\a.in a B);
claim singletonprop:!A:V.!phi:V>*.(!a:V.in a A>!b:V.in b A>phi a>phi b>eq a b)>dex A (\a.phi a)>singleton (dsetconstr A (\a.phi a)); (proof)
claim ex1I2:!A:V.!phi:V>*.(!a:V.in a A>!b:V.in b A>phi a>phi b>eq a b)>dex A (\a.phi a)>ex1 A (\a.phi a); (proof)
claim singletonsswitch:!x:V.!y:V.in x (setadjoin y emptyset)>in y (setadjoin x emptyset); (proof)
def stricttotalorderedByIn:V>*=\A.and (and (dall A (\a.dall A (\b.dall A (\c.imp (and (in a b) (in b c)) (in a c))))) (dall A (\a.dall A (\b.or (eq a b) (or (in a b) (in b a)))))) (dall A (\a.not (in a a)));
claim subPowSU:!A:V.!a:V.in a A>in a (powerset (setunion A)); (proof)
claim subsetE2:!A:V.!B:V.!x:V.subset A B>not (in x B)>not (in x A); (proof)
claim subsetRefl:!A:V.subset A A; (proof)
claim inPowerset:!A:V.in A (powerset A); (proof)
claim subsetTrans:!A:V.!B:V.!C:V.subset A B>subset B C>subset A C; (proof)
claim setadjoinSub2:!A:V.!x:V.!B:V.subset A B>subset A (setadjoin x B); (proof)
claim subsetemptysetimpeq:!A:V.subset A emptyset>eq A emptyset; (proof)
claim noeltsimpempty:!A:V.(!x:V.not (in x A))>eq A emptyset; (proof)
claim setminusSubset2:!A:V.!B:V.subset A B>eq (setminus A B) emptyset; (proof)
def surjective:V>V>V>*=\A.\B.\f.dall B (\b.dex A (\a.eq (ap A B f a) b));
def surjFuncSet:V>V>V=\A.\B.dsetconstr (funcSet A B) (\f.surjective A B f);
claim surjFuncSetFuncIn:!A:V.!B:V.!f:V.in f (surjFuncSet A B)>in f (funcSet A B); (proof)
claim surjFuncSetFuncSurj:!x:V.!y:V.!f:V.in f (surjFuncSet x y)>surjective x y f; (proof)
claim leftInvIsSurj:!A:V.!B:V.!f:V>V.(!a:V.in a A>in (f a) B)>!g:V.in g (funcSet B A)>dall A (\a.eq (ap B A g (f a)) a)>surjective B A g; (proof)
claim surjCantorThm:!A:V.!f:V.in f (funcSet A (powerset A))>not (surjective A (powerset A) f); (proof)
def symdiff:V>V>V=\A.\B.dsetconstr (binunion A B) (\x.or (not (in x A)) (not (in x B)));
claim symdiffE:!A:V.!B:V.!x:V.in x (symdiff A B)>!phi:*.(in x A>not (in x B)>phi)>(not (in x A)>in x B>phi)>phi; (proof)
claim symdiffI1:!A:V.!B:V.!x:V.in x A>not (in x B)>in x (symdiff A B); (proof)
claim symdiffI2:!A:V.!B:V.!x:V.not (in x A)>in x B>in x (symdiff A B); (proof)
claim symdiffIneg1:!A:V.!B:V.!x:V.in x A>in x B>not (in x (symdiff A B)); (proof)
claim symdiffIneg2:!A:V.!B:V.!x:V.not (in x A)>not (in x B)>not (in x (symdiff A B)); (proof)
def transitive:V>V>*=\A.\R.dall A (\a.dall A (\b.dall A (\c.imp (and (in (kpair a b) R) (in (kpair b c) R)) (in (kpair a c) R))));
def refllinearorder:V>V>*=\A.\R.and (and (and (reflexive A R) (transitive A R)) (antisymmetric A R)) (dall A (\a.dall A (\b.or (in (kpair a b) R) (in (kpair b a) R))));
def refltransitive:V>V>*=\A.\R.and (reflexive A R) (transitive A R);
def reflwellordering:V>V>*=\A.\R.and (refllinearorder A R) (dall (powerset A) (\X.imp (nonempty X) (dex X (\x.dall X (\y.in (kpair x y) R)))));
claim choice2fnsingleton:!A:V.!B:V.!phi:V>V>*.dall A (\a.dex B (\b.phi a b))>!R:V.in R (breln1Set B)>reflwellordering B R>!a:V.in a A>singleton (dsetconstr B (\b.and (phi a b) (dall B (\c.imp (phi a c) (in (kpair b c) R))))); (proof)
def transitiveset:V>*=\A.dall A (\a.subset a A);
claim transitivesetOp1:!X:V.transitiveset X>!A:V.in A X>subset A X; (proof)
claim binintTransitive:!X:V.transitiveset X>!Y:V.transitiveset Y>transitiveset (binintersect X Y); (proof)
claim transitivesetOp2:!X:V.transitiveset X>!A:V.!x:V.in A X>in x A>in x X; (proof)
claim setunionTransitive:!X:V.dall X (\x.transitiveset x)>transitiveset (setunion X); (proof)
claim upairsetE:!x:V.!y:V.!z:V.in z (setadjoin x (setadjoin y emptyset))>or (eq z x) (eq z y); (proof)
claim upairsetIL:!x:V.!y:V.in x (setadjoin x (setadjoin y emptyset)); (proof)
claim upairsetIR:!x:V.!y:V.in y (setadjoin x (setadjoin y emptyset)); (proof)
def upairsetp:V>*=\x.and (atleast2p x) (atmost2p x);
claim vacuousDall:!phi:V>*.dall emptyset (\x.phi x); (proof)
def wellorderedByIn:V>*=\A.and (stricttotalorderedByIn A) (dall (powerset A) (\X.imp (nonempty X) (dex X (\x.dall X (\Y.or (eq x Y) (in x Y))))));
def ordinal:V>*=\x.and (transitiveset x) (wellorderedByIn x);
def limitOrdinal:V>*=\A.and (ordinal A) (dall A (\a.dex A (\b.in a b)));
claim ordinalMinLem1:!X:V.ordinal X>!Y:V.ordinal Y>transitiveset (binintersect X Y); (proof)
claim ordinalTransSet:!X:V.ordinal X>!x:V.!A:V.in A X>in x A>in x X; (proof)
claim ordinalTransSet1:!X:V.ordinal X>!A:V.in A X>subset A X; (proof)
claim setunionOrdinalLem1:!X:V.dall X (\x.ordinal x)>transitiveset (setunion X); (proof)
def succOrdinal:V>*=\A.and (ordinal A) (dex A (\a.eq A (setadjoin a a)));
claim emptysetOrdinal:ordinal emptyset; (proof)
claim ordinalIrrefl:!X:V.ordinal X>!A:V.in A X>not (in A A); (proof)
claim ordinalIrrefl2:!X:V.ordinal X>not (in X X); (proof)
claim ordinalNoCycle:!X:V.ordinal X>!A:V.in X A>not (in A X); (proof)
claim ordinalTransIn:!X:V.ordinal X>!x:V.!A:V.!B:V.in x A>in A B>in B X>in x B; (proof)
Simptcheck: Simple Proof Term Checker in OCaml
Automated Reasoning in Higher Order Logic
Javascript Interactive Higher-Order Theorem Prover
