def A:V;
def B:V;
claim BsubPA:subset B (powerset A);
def R0:V;
claim R0subAA:!g:V.in g R0>in g (funcSet A A);
def pi:V>V;
claim pi:!x:V.in x A>in (pi x) B;
claim emptyinB:in emptyset B;
claim AinB:in A B;
claim complB:!X:V.in X B>in (setminus A X) B;
claim unionB:!X:V.in X B>!Y:V.in Y B>in (binunion X Y) B;
claim pi_inj:!x:V.in x A>!y:V.in y A>eq (pi x) (pi y)>eq x y;
claim pi_surj:!X:V.in X B>dex A (\x.eq (pi x) X);
claim KinR0:!x:V.in x A>in (lam A A (\y.x)) R0;
def D1:V=dsetconstr (powerset A) (\X.dall R0 (\g.in (dsetconstr A (\x.in (ap A A g x) X)) B));
def R1:V=dsetconstr (funcSet A D1) (\G.dall R0 (\g.in (dsetconstr A (\x.in (ap A A g x) (ap A D1 G x))) B));
def D2:V=dsetconstr (powerset D1) (\W.dall R1 (\G.in (dsetconstr A (\x.in (ap A D1 G x) W)) B));
def R2:V=dsetconstr (funcSet A D2) (\k.dall R1 (\G.in (dsetconstr A (\x.in (ap A D1 G x) (ap A D2 k x))) B));
def D3:V=dsetconstr (powerset D2) (\Z.dall R2 (\k.in (dsetconstr A (\x.in (ap A D2 k x) Z)) B));
def R3:V=dsetconstr (funcSet A D3) (\K.dall R2 (\k.in (dsetconstr A (\x.in (ap A D2 k x) (ap A D3 K x))) B));
def D4:V=dsetconstr (powerset D3) (\C.dall R3 (\K.in (dsetconstr A (\x.in (ap A D3 K x) C)) B));
def R4:V=dsetconstr (funcSet A D4) (\q.dall R3 (\K.in (dsetconstr A (\x.in (ap A D3 K x) (ap A D4 q x))) B));
def pi1:V>V=\X.dsetconstr D1 (\Y.dex A (\x.and (in x X) (eq (pi x) Y)));
def pi2:V>V=\W.dsetconstr D2 (\U.dex D1 (\X.and (in X W) (eq (pi1 X) U)));
claim condA:!g:V.in g R0>!X:V.in X B>in (dsetconstr A (\x.in (ap A A g x) X)) B;
claim condB:in (lam A A (\x.x)) R0;
claim condC1:!G:V.in G R1>!X:V.in X B>in (dsetconstr A (\x.dex A (\y.and (in y X) (eq (ap A D1 G y) (pi y))))) B;
claim condC2:!k:V.in k R2>!W:V.in W D2>in (dsetconstr A (\x.in (ap A D2 k x) (pi2 W))) B;
claim condD1:!W:V.in W D2>in (dsetconstr A (\x.in (pi x) W)) B;
claim condD2:!Z:V.in Z D3>in (dsetconstr D1 (\X.in (pi1 X) Z)) D2;
claim condE0:!g:V.in g R0>!h:V.in h R0>in (dsetconstr A (\x.eq (ap A A g x) (ap A A h x))) B;
claim condE1:!G:V.in G R1>!H:V.in H R1>in (dsetconstr A (\x.eq (ap A D1 G x) (ap A D1 H x))) B;
claim condE2:!k:V.in k R2>!j:V.in j R2>in (dsetconstr A (\x.eq (ap A D2 k x) (ap A D2 j x))) B;
claim condE3:!K:V.in K R3>!J:V.in J R3>in (dsetconstr A (\x.eq (ap A D3 K x) (ap A D3 J x))) B;
claim condE4:!q:V.in q R4>!p:V.in p R4>in (dsetconstr A (\x.eq (ap A D4 q x) (ap A D4 p x))) B;