zfc basics, in simptcheck syntax

Proofs

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

Simptcheck: Simple Proof Term Checker in OCaml

Javascript Interactive Higher-Order Theorem Prover

Automated Reasoning in Higher Order Logic