% Author: Chad E Brown
% March 2008
% Classical FO logic with descriptions + ZFC set theory
% This version corresponds to the detset entries on the mathgate site
const 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;
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;
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;
claim falseE:!phi:*.false>phi;
claim notI:!phi:*.(phi>false)>not phi;
claim contradiction:!phi:*.(not phi>false)>phi;
claim dnegE:!phi:*.not (not phi)>phi;
claim dnegI:!phi:*.phi>not (not phi);
claim contrapositive1:!phi:*.!psi:*.(phi>psi)>not psi>not phi;
claim contrapositive2:!phi:*.!psi:*.(not phi>psi)>not psi>phi;
claim contrapositive3:!phi:*.!psi:*.(not phi>not psi)>psi>phi;
claim contrapositive4:!phi:*.!psi:*.(phi>not psi)>psi>not phi;
claim andI:!phi:*.!psi:*.phi>psi>and phi psi;
claim andEL:!phi:*.!psi:*.and phi psi>phi;
claim andER:!phi:*.!psi:*.and phi psi>psi;
claim orIL:!phi:*.!psi:*.phi>or phi psi;
claim orIR:!phi:*.!psi:*.psi>or phi psi;
claim orE:!phi:*.!psi:*.or phi psi>!theta:*.(phi>theta)>(psi>theta)>theta;
claim orIDemorgan:!phi:*.!psi:*.(not phi>not psi>false)>or phi psi;
claim exE:!phi:V>*.ex (\x.phi x)>!psi:*.(!x:V.phi x>psi)>psi;
claim exI:!phi:V>*.!x:V.phi x>ex (\y.phi y);
claim equivI:!phi:*.!psi:*.(phi>psi)>(psi>phi)>equiv phi psi;
claim equivE:!phi:*.!psi:*.!theta:*.equiv phi psi>(phi>psi>theta)>(not phi>not psi>theta)>theta;
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;
claim eqI:!x:V.eq x x;
claim setadjoinIL:!x:V.!y:V.in x (setadjoin x y);
claim setadjoinIR:!x:V.!A:V.!y:V.in y A>in y (setadjoin x A);
claim setadjoinE:!x:V.!A:V.!y:V.in y (setadjoin x A)>!phi:*.(eq y x>phi)>(in y A>phi)>phi;
def true:*=in emptyset (setadjoin emptyset emptyset);
claim trueI:true;
claim powersetI:!A:V.!B:V.(!x:V.in x B>in x A)>in B (powerset A);
claim powersetE:!A:V.!B:V.!x:V.in B (powerset A)>in x B>in x A;
claim setunionI:!A:V.!x:V.!B:V.in x B>in B A>in x (setunion A);
claim setunionE:!A:V.!x:V.in x (setunion A)>!phi:*.(!B:V.in x B>in B A>phi)>phi;
claim symeq:!x:V.!y:V.eq x y>eq y x;
claim transeq:!x:V.!y:V.!z:V.eq x y>eq y z>eq x z;
claim eqE2:!x:V.!y:V.!phi:V>*.eq x y>phi y>phi x;
claim symtrans1eq:!x:V.!y:V.!z:V.eq x y>eq z y>eq x z;
claim uniqinunit:!x:V.!y:V.in x (setadjoin y emptyset)>eq x y;
claim eqinunit:!x:V.!y:V.eq x y>in x (setadjoin y emptyset);
claim symtrans2eq:!x:V.!y:V.!z:V.eq x y>eq z y>eq z x;
claim boxeq:!x:V.!y:V.!z:V.!u:V.eq x y>eq z u>eq y u>eq x z;
claim dallI:!A:V.!phi:V>*.(!a:V.in a A>phi a)>dall A (\a.phi a);
claim dallE:!A:V.!phi:V>*.dall A (\a.phi a)>!a:V.in a A>phi a;
claim dexI:!A:V.!phi:V>*.!a:V.in a A>phi a>dex A (\b.phi b);
claim dexE:!A:V.!phi:V>*.dex A (\a.phi a)>!psi:*.(!a:V.in a A>phi a>psi)>psi;
claim prop2setI:!phi:*.phi>in emptyset (prop2set phi);
claim dandI:!phi:*.!psi:*.phi>psi>dand phi psi;
claim dandEL:!phi:*.!psi:*.dand phi psi>phi;
claim dandER:!phi:*.!psi:*.dand phi psi>psi;
claim dimpI:!phi:*.!psi:*.(phi>psi)>dimp phi psi;
claim dimpE:!phi:*.!psi:*.dimp phi psi>phi>psi;
claim vacuousImpI:!phi:*.!psi:*.not phi>imp phi psi;
claim trivialImpI:!phi:*.!psi:*.psi>imp phi psi;
claim excludedmiddle:!phi:*.or phi (not phi);
claim notimpE:!phi:*.!psi:*.not (imp phi psi)>and phi (not psi);
claim notimpE1:!phi:*.!psi:*.not (imp phi psi)>phi;
claim notimpE2:!phi:*.!psi:*.not (imp phi psi)>not psi;
claim notorE:!phi:*.!psi:*.not (or phi psi)>and (not phi) (not psi);
claim notorE1:!phi:*.!psi:*.not (or phi psi)>not phi;
claim notorE2:!phi:*.!psi:*.not (or phi psi)>not psi;
claim notandE:!phi:*.!psi:*.not (and phi psi)>or (not phi) (not psi);
claim notexE:!phi:V>*.not (ex (\x.phi x))>all (\x.not (phi x));
claim notdexE:!A:V.!phi:V>*.not (dex A (\a.phi a))>dall A (\a.not (phi a));
claim notallE:!phi:V>*.not (all (\x.phi x))>ex (\x.not (phi x));
claim notdallE:!A:V.!phi:V>*.not (dall A (\a.phi a))>dex A (\a.not (phi a));
claim reflequiv:!phi:*.equiv phi phi;
claim symequiv:!phi:*.!psi:*.equiv phi psi>equiv psi phi;
claim transequiv:!phi:*.!psi:*.!theta:*.equiv phi psi>equiv psi theta>equiv phi theta;
claim symtrans1equiv:!phi:*.!psi:*.!theta:*.equiv phi psi>equiv theta psi>equiv phi theta;
claim boxequiv:!phi:*.!psi:*.!theta:*.!xi:*.equiv phi psi>equiv theta xi>equiv psi xi>equiv phi theta;
claim eqCE:!phi:V>*.!x:V.phi x>!y:V.phi y>!psi:V>*.eq x y>psi x>psi y;
claim eqCE2:!phi:V>*.!x:V.phi x>!y:V.phi y>!psi:V>*.eq x y>psi y>psi x;
claim inCongP:!A:V.!B:V.eq A B>!x:V.!y:V.eq x y>in x A>in y B;
claim in__Cong:!A:V.!B:V.eq A B>!x:V.!y:V.eq x y>equiv (in x A) (in y B);
claim eqCongP:!x:V.!y:V.eq x y>!z:V.!u:V.eq z u>eq x z>eq y u;
claim eq__Cong:!x:V.!y:V.eq x y>!z:V.!u:V.eq z u>equiv (eq x z) (eq y u);
claim notCongP:!phi:*.!psi:*.equiv phi psi>not phi>not psi;
claim not__Cong:!phi:*.!psi:*.equiv phi psi>equiv (not phi) (not psi);
claim imp__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (imp phi theta) (imp psi xi);
claim equiv__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (equiv phi theta) (equiv psi xi);
claim and__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (and phi theta) (and psi xi);
claim or__Cong:!phi:*.!psi:*.equiv phi psi>!theta:*.!xi:*.equiv theta xi>equiv (or phi theta) (or psi xi);
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));
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));
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));
claim emptyset__Cong:eq emptyset emptyset;
claim setadjoin__Cong:!x:V.!y:V.eq x y>!z:V.!u:V.eq z u>eq (setadjoin x z) (setadjoin y u);
claim powerset__Cong:!A:V.!B:V.eq A B>eq (powerset A) (powerset B);
claim setunion__Cong:!A:V.!B:V.eq A B>eq (setunion A) (setunion B);
claim omega__Cong:eq omega omega;
claim exuEu:!phi:V>*.exu (\x.phi x)>!x:V.!y:V.phi x>phi y>eq x y;
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));
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));
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;
claim subsetI2:!A:V.!B:V.(!x:V.in x A>in x B)>subset A B;
claim subsetE:!A:V.!B:V.!x:V.subset A B>in x A>in x B;
claim subset2powerset:!A:V.!B:V.subset A B>in A (powerset B);
claim setextsub:!A:V.!B:V.subset A B>subset B A>eq A B;
claim powersetI1:!A:V.!B:V.subset B A>in B (powerset A);
claim powersetsubset:!A:V.!B:V.subset A B>subset (powerset A) (powerset B);
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);
claim upairset2IR:!x:V.!y:V.in y (setadjoin x (setadjoin y emptyset));
claim binunionIR:!A:V.!B:V.!x:V.in x B>in x (binunion A B);
claim binunionEcases:!A:V.!B:V.!x:V.!phi:*.in x (binunion A B)>(in x A>phi)>(in x B>phi)>phi;
claim binunionE:!A:V.!B:V.!x:V.in x (binunion A B)>or (in x A) (in x B);
claim binunionLsub:!A:V.!B:V.subset A (binunion A B);
claim binunionRsub:!A:V.!B:V.subset B (binunion A B);
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);
claim binintersectEL:!A:V.!B:V.!x:V.in x (binintersect A B)>in x A;
claim binintersectER:!A:V.!B:V.!x:V.in x (binintersect A B)>in x B;
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));
claim setukpairIL:!x:V.!y:V.in x (setunion (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)));
claim setukpairIR:!x:V.!y:V.in y (setunion (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset)));
claim kpairiskpair:!x:V.!y:V.iskpair (setadjoin (setadjoin x emptyset) (setadjoin (setadjoin x (setadjoin y emptyset)) emptyset));
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);
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;
claim singletoninpowerset:!A:V.!a:V.in a A>in (setadjoin a emptyset) (powerset A);
claim singletoninpowunion:!A:V.!B:V.!a:V.in a A>in (setadjoin a emptyset) (powerset (binunion A B));
claim upairset2E:!x:V.!y:V.!z:V.in z (setadjoin x (setadjoin y emptyset))>or (eq z x) (eq z y);
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);
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));
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));
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)));
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)));
claim cartprodpairin:!A:V.!B:V.!a:V.in a A>!b:V.in b B>in (kpair a b) (cartprod A B);
claim cartprodmempair1:!A:V.!B:V.!u:V.in u (cartprod A B)>dex A (\a.dex B (\b.eq u (kpair a b)));
claim cartprodmempair:!A:V.!B:V.!u:V.in u (cartprod A B)>iskpair u;
claim setunionE2:!A:V.!x:V.in x (setunion A)>dex A (\a.in x a);
claim setunionsingleton1:!A:V.subset (setunion (setadjoin A emptyset)) A;
claim setunionsingleton2:!A:V.subset A (setunion (setadjoin A emptyset));
claim setunionsingleton:!x:V.eq (setunion (setadjoin x emptyset)) x;
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);
claim singletonsuniq:!x:V.!y:V.eq (setadjoin x emptyset) (setadjoin y emptyset)>eq x y;
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;
claim kfstsingleton:!u:V.iskpair u>singleton (dsetconstr (setunion u) (\x.in (setadjoin x emptyset) u));
claim theprop:!X:V.singleton X>in (setunion X) X;
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;
claim cartprodfstin:!A:V.!B:V.!u:V.in u (cartprod A B)>in (kfst u) A;
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;
claim setukpairinjR11:!x:V.!y:V.eq x y>eq (setadjoin x (setadjoin y emptyset)) (setadjoin x emptyset);
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);
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;
claim upairequniteq:!x:V.!y:V.!z:V.eq (setadjoin x (setadjoin y emptyset)) (setadjoin z emptyset)>eq x y;
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;
claim setukpairinjR:!x:V.!y:V.!z:V.!u:V.eq (kpair x y) (kpair z u)>eq y u;
claim ksndsingleton:!u:V.iskpair u>singleton (dsetconstr (setunion u) (\x.eq u (kpair (kfst u) x)));
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;
claim cartprodsndin:!A:V.!B:V.!u:V.in u (cartprod A B)>in (ksnd u) B;
claim cartprodmempaircEq:!A:V.!B:V.!a:V.in a A>!b:V.in b B>eq (kpair a b) (kpair a b);
claim cartprodfstpairEq:!A:V.!B:V.!a:V.in a A>!b:V.in b B>eq (kfst (kpair a b)) a;
claim cartprodsndpairEq:!A:V.!B:V.!a:V.in a A>!b:V.in b B>eq (ksnd (kpair a b)) b;
claim cartprodpairsurjEq:!A:V.!B:V.!u:V.in u (cartprod A B)>eq (kpair (kfst u) (ksnd u)) u;
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));
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;
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;
claim infuncsetfunc:!A:V.!B:V.!f:V.in f (funcSet A B)>func A B f;
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;
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));
claim dpsetconstrSub:!A:V.!B:V.!phi:V>V>*.subset (dpsetconstr A B (\a.\b.phi a b)) (cartprod A B);
claim funcinfuncset:!A:V.!B:V.!f:V.func A B f>in f (funcSet A B);
claim setOfPairsIsBReln:!A:V.!B:V.!phi:V>V>*.breln A B (dpsetconstr A B (\a.\b.phi a b));
claim setukpairinjL:!x:V.!y:V.!z:V.!u:V.eq (kpair x y) (kpair z u)>eq x z;
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;
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));
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));
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);
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);
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;
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;
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;
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;
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;
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;
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;
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);
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);
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));
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);
claim eta2:!A:V.!B:V.!f:V.in f (funcSet A B)>eq (lam A B (\a.ap A B f a)) f;
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))));
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);
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))));
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);
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))));
claim powersetE1:!A:V.!B:V.in B (powerset A)>subset B A;
claim sepInPowerset:!A:V.!phi:V>*.in (dsetconstr A (\a.phi a)) (powerset A);
claim sepSubset:!A:V.!phi:V>*.subset (dsetconstr A (\a.phi a)) A;
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;
claim theeq:!X:V.singleton X>!x:V.in x X>eq (setunion X) x;
claim iftrue:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>phi>eq (if A phi a b) a;
claim iffalse:!A:V.!phi:*.!a:V.in a A>!b:V.in b A>not phi>eq (if A phi a b) b;
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));
claim bs114d:!A:V.!B:V.!C:V.eq (binintersect A (binunion B C)) (binunion (binintersect A B) (binintersect A C));
claim binintersectT_lem:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (binintersect X Y) (powerset A);
claim binunionT_lem:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (binunion X Y) (powerset A);
claim powersetT_lem:!A:V.!X:V.in X (powerset A)>in (powerset X) (powerset (powerset A));
claim setminusEL:!A:V.!B:V.!x:V.in x (setminus A B)>in x A;
claim setminusT_lem:!A:V.!X:V.in X (powerset A)>!Y:V.in Y (powerset A)>in (setminus X Y) (powerset A);
claim complementT_lem:!A:V.!X:V.in X (powerset A)>in (setminus A X) (powerset A);
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;
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;
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);
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;
claim setminusI:!A:V.!B:V.!x:V.in x A>not (in x B)>in x (setminus A B);
claim setminusER:!A:V.!B:V.!x:V.in x (setminus A B)>not (in x B);
claim complementTI1:!A:V.!X:V.in X (powerset A)>!a:V.in a A>in a X>not (in a (setminus A X));
claim complementTE1:!A:V.!X:V.in X (powerset A)>!a:V.in a A>not (in a (setminus A X))>in a X;
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));
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));
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);
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);
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);
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;
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));
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;
claim doubleComplementSub1:!A:V.!X:V.in X (powerset A)>subset X (setminus A (setminus A X));
claim doubleComplementSub2:!A:V.!X:V.in X (powerset A)>subset (setminus A (setminus A X)) X;
claim doubleComplementEq:!A:V.!X:V.in X (powerset A)>eq X (setminus A (setminus A X));
claim binintersectLsub:!A:V.!B:V.subset (binintersect A B) A;
claim binintersectRsub:!A:V.!B:V.subset (binintersect A B) B;
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));
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));
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));
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)));
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);
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);
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);
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);
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);
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);
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));
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)));
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);
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);
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;
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));
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);
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);
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));
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));
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));
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));
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));
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));
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));
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;
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;
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;
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);
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);
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)));
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)));
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)));
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);
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));
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);
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;
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;
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));
claim breln1invprop:!A:V.!R:V.breln1 A R>breln1 A (breln1invset A R);
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);
claim cartprodpairmemEL:!A:V.!B:V.!x:V.!y:V.in (kpair x y) (cartprod A B)>in x A;
claim cartprodpairmemER:!A:V.!B:V.!x:V.!y:V.in (kpair x y) (cartprod A B)>in y B;
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;
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;
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;
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;
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);
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);
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));
claim breln1unionprop:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>breln1 A (binunion R S);
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);
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);
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);
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);
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;
claim breln1unionCommutes:!A:V.!R:V.breln1 A R>!S:V.breln1 A S>eq (binunion R S) (binunion S R);
claim woz2Ex:!A:V.!R:V.breln1 A R>eq R (breln1invset A (breln1invset A R));
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));
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));
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))));
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);
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;
claim binintersectSubset2:!A:V.!B:V.subset A B>eq (binintersect A B) A;
claim binintersectSubset3:!A:V.!B:V.eq (binintersect A B) B>subset B A;
claim binintersectSubset4:!A:V.!B:V.subset B A>eq (binintersect A B) B;
claim binintersectSubset5:!A:V.!B:V.!C:V.subset C A>subset C B>subset C (binintersect A B);
claim boolDeMorgan1:!phi:*.!psi:*.not (and phi psi)>or (not phi) (not psi);
claim boolDeMorgan2:!phi:*.!psi:*.or (not phi) (not psi)>not (and phi psi);
claim boolDeMorgan3:!phi:*.!psi:*.not (or phi psi)>and (not phi) (not psi);
claim boolDeMorgan3a:!phi:*.!psi:*.not (imp phi psi)>and phi (not psi);
claim boolDeMorgan4:!phi:*.!psi:*.and (not phi) (not psi)>not (or phi psi);
claim boolDeMorgan4a:!phi:*.!psi:*.and phi (not psi)>not (imp phi psi);
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;
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;
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);
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);
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));
claim contrapositive1a:!phi:*.!psi:*.imp phi psi>not psi>not phi;
claim contrapositive2a:!phi:*.!psi:*.imp (not phi) psi>not psi>phi;
claim contrapositive3a:!phi:*.!psi:*.imp (not phi) (not psi)>psi>phi;
claim contrapositive4a:!phi:*.!psi:*.imp phi (not psi)>psi>not phi;
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;
claim emptyI:!A:V.(!x:V.not (in x A))>eq A emptyset;
claim disjointsetsI1:!A:V.!B:V.not (ex (\x.and (in x A) (in x B)))>eq (binintersect A B) emptyset;
claim emptyInPowerset:!A:V.in emptyset (powerset A);
claim emptyinPowerset:!A:V.in emptyset (powerset A);
claim emptyinunitempty:in emptyset (setadjoin emptyset emptyset);
claim emptysetimpfalse:!x:V.in x emptyset>false;
claim emptysetsubset:!A:V.subset emptyset A;
claim eqET:!A:V.!a:V.in a A>!b:V.in b A>eq a b>!phi:V>*.phi a>phi b;
claim eqET2:!A:V.!a:V.in a A>!b:V.in b A>eq a b>!phi:V>*.phi b>phi a;
claim eqimpsubset1:!A:V.!B:V.eq A B>subset A B;
claim eqimpsubset2:!A:V.!B:V.eq A B>subset B A;
claim equivAndE1:!phi:*.!psi:*.!theta:*.equiv phi (and psi theta)>phi>psi;
claim equivAndE2:!phi:*.!psi:*.!theta:*.equiv phi (and psi theta)>phi>theta;
claim equivAndE3:!phi:*.!psi:*.!theta:*.equiv phi (and psi theta)>psi>theta>phi;
claim equivOrE1:!phi:*.!psi:*.!theta:*.equiv phi (or psi theta)>psi>phi;
claim equivOrE2:!phi:*.!psi:*.!theta:*.equiv phi (or psi theta)>theta>phi;
claim eta1:!A:V.!B:V.!f:V.func A B f>eq (lam A B (\a.ap A B f a)) f;
claim ex1E1:!A:V.!phi:V>*.ex1 A (\a.phi a)>dex A (\a.phi a);
claim exuE1:!phi:V>*.exu (\x.phi x)>ex (\x.and (phi x) (all (\y.imp (phi y) (eq x y))));
claim exuE2:!phi:V>*.exu (\x.phi x)>ex (\x.all (\y.equiv (phi y) (eq y x)));
claim exuE3e:!phi:V>*.exu (\x.phi x)>ex (\x.phi x);
claim exuE3u:!phi:V>*.exu (\x.phi x)>!x:V.!y:V.phi x>phi y>eq x y;
claim exuI1:!phi:V>*.ex (\x.and (phi x) (all (\y.imp (phi y) (eq x y))))>exu (\x.phi x);
claim exuI2:!phi:V>*.ex (\x.all (\y.equiv (phi y) (eq y x)))>exu (\x.phi x);
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);
claim emptynotinempty:not (in emptyset emptyset);
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;
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;
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;
claim image1Ex:!A:V.!f:V>V.ex (\B.all (\x.equiv (in x B) (dex A (\a.eq x (f a)))));
claim image1Ex1:!A:V.!f:V>V.exu (\B.all (\x.equiv (in x B) (dex A (\a.eq x (f a)))));
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)));
claim image1E:!A:V.!f:V>V.!x:V.in x (image1 A (\a.f a))>dex A (\a.eq x (f a));
claim image1I:!A:V.!f:V>V.!x:V.dex A (\a.eq x (f a))>in x (image1 A (\a.f a));
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);
claim injFuncSetFuncIn:!A:V.!B:V.!f:V.in f (injFuncSet A B)>in f (funcSet A B);
claim injFuncSetFuncInj:!x:V.!y:V.!f:V.in f (injFuncSet x y)>injective x y f;
claim kpairsurjEq:!u:V.iskpair u>eq (kpair (kfst u) (ksnd u)) u;
def nonempty:V>*=\x.not (eq x emptyset);
claim nonemptyE1:!A:V.nonempty A>ex (\x.in x A);
claim foundation2:!A:V.imp (nonempty A) (dex A (\a.eq (binintersect a A) emptyset));
claim nonemptyI:!A:V.!phi:V>*.!a:V.in a A>phi a>nonempty (dsetconstr A (\b.phi b));
claim nonemptyI1:!A:V.ex (\x.in x A)>nonempty A;
claim notequalI1:!A:V.!B:V.not (subset A B)>not (eq A B);
claim notfalse:not false;
claim notinemptyset:!x:V.not (in x emptyset);
claim notinself:!A:V.not (in A A);
claim notinself2:!A:V.!B:V.in A B>not (in B A);
claim notinsingleton:!x:V.!y:V.not (eq x y)>not (in y (setadjoin x emptyset));
claim notsubsetI:!A:V.!B:V.!x:V.in x A>not (in x B)>not (subset A B);
claim notequalI2:!A:V.!B:V.!x:V.in x A>not (in x B)>not (eq A B);
def omegaS:V>V=\x.setadjoin x x;
claim omegaSp:!x:V.in x omega>in (omegaS x) omega;
claim omegaSclos:!x:V.in x omega>in (setadjoin x x) omega;
claim peano0notS:!x:V.in x omega>not (eq (omegaS x) emptyset);
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;
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));
claim quantDeMorgan2:!A:V.!phi:V>*.dall A (\a.not (phi a))>not (dex A (\a.phi a));
claim quantDeMorgan3:!A:V.!phi:V>*.not (dex A (\a.phi a))>dall A (\a.not (phi a));
claim quantDeMorgan4:!A:V.!phi:V>*.dex A (\a.not (phi a))>not (dall A (\a.phi a));
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);
claim setadjoinOr:!x:V.!A:V.!y:V.in y (setadjoin x A)>or (eq y x) (in y A);
claim setadjoinSub:!x:V.!A:V.subset A (setadjoin x A);
claim setbeta:!A:V.!phi:V>*.!a:V.in a A>equiv (in a (dsetconstr A (\b.phi b))) (phi a);
claim setminusERneg:!A:V.!B:V.!x:V.not (in x (setminus A B))>in x A>in x B;
claim setminusELneg:!A:V.!B:V.!x:V.not (in x (setminus A B))>not (in x B)>not (in x A);
claim setminusILneg:!A:V.!B:V.!x:V.not (in x A)>not (in x (setminus A B));
claim setminusIRneg:!A:V.!B:V.!x:V.in x B>not (in x (setminus A B));
claim setminusLsub:!A:V.!B:V.subset (setminus A B) A;
claim setminusSubset1:!A:V.!B:V.eq (setminus A B) emptyset>subset A B;
claim setoftrueEq:!A:V.eq (dsetconstr A (\a.true)) A;
claim nonemptyImpWitness:!A:V.nonempty A>dex A (\a.true);
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));
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);
claim singletonsswitch:!x:V.!y:V.in x (setadjoin y emptyset)>in y (setadjoin x emptyset);
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));
claim subsetE2:!A:V.!B:V.!x:V.subset A B>not (in x B)>not (in x A);
claim subsetRefl:!A:V.subset A A;
claim inPowerset:!A:V.in A (powerset A);
claim subsetTrans:!A:V.!B:V.!C:V.subset A B>subset B C>subset A C;
claim setadjoinSub2:!A:V.!x:V.!B:V.subset A B>subset A (setadjoin x B);
claim subsetemptysetimpeq:!A:V.subset A emptyset>eq A emptyset;
claim noeltsimpempty:!A:V.(!x:V.not (in x A))>eq A emptyset;
claim setminusSubset2:!A:V.!B:V.subset A B>eq (setminus A B) emptyset;
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);
claim surjFuncSetFuncSurj:!x:V.!y:V.!f:V.in f (surjFuncSet x y)>surjective x y f;
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;
claim surjCantorThm:!A:V.!f:V.in f (funcSet A (powerset A))>not (surjective A (powerset A) f);
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;
claim symdiffI1:!A:V.!B:V.!x:V.in x A>not (in x B)>in x (symdiff A B);
claim symdiffI2:!A:V.!B:V.!x:V.not (in x A)>in x B>in x (symdiff A B);
claim symdiffIneg1:!A:V.!B:V.!x:V.in x A>in x B>not (in x (symdiff A B));
claim symdiffIneg2:!A:V.!B:V.!x:V.not (in x A)>not (in x B)>not (in x (symdiff A B));
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)))));
def transitiveset:V>*=\A.dall A (\a.subset a A);
claim transitivesetOp1:!X:V.transitiveset X>!A:V.in A X>subset A X;
claim binintTransitive:!X:V.transitiveset X>!Y:V.transitiveset Y>transitiveset (binintersect X Y);
claim transitivesetOp2:!X:V.transitiveset X>!A:V.!x:V.in A X>in x A>in x X;
claim setunionTransitive:!X:V.dall X (\x.transitiveset x)>transitiveset (setunion X);
claim upairsetE:!x:V.!y:V.!z:V.in z (setadjoin x (setadjoin y emptyset))>or (eq z x) (eq z y);
claim upairsetIL:!x:V.!y:V.in x (setadjoin x (setadjoin y emptyset));
claim upairsetIR:!x:V.!y:V.in y (setadjoin x (setadjoin y emptyset));
def upairsetp:V>*=\x.and (atleast2p x) (atmost2p x);
claim vacuousDall:!phi:V>*.dall emptyset (\x.phi x);
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);
claim ordinalTransSet:!X:V.ordinal X>!x:V.!A:V.in A X>in x A>in x X;
claim ordinalTransSet1:!X:V.ordinal X>!A:V.in A X>subset A X;
claim setunionOrdinalLem1:!X:V.dall X (\x.ordinal x)>transitiveset (setunion X);
def succOrdinal:V>*=\A.and (ordinal A) (dex A (\a.eq A (setadjoin a a)));
claim emptysetOrdinal:ordinal emptyset;
claim ordinalIrrefl:!X:V.ordinal X>!A:V.in A X>not (in A A);
claim ordinalIrrefl2:!X:V.ordinal X>not (in X X);
claim ordinalNoCycle:!X:V.ordinal X>!A:V.in X A>not (in A X);
claim ordinalTransIn:!X:V.ordinal X>!x:V.!A:V.!B:V.in x A>in A B>in B X>in x B;