let A be Subset of [:NAT,NAT:]; :: thesis: proj2 A = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }

set A2 = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ;

A1: proj2 A c= { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }

set A2 = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ;

A1: proj2 A c= { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }

proof

{ y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } c= proj2 A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 A or y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } )

assume y in proj2 A ; :: thesis: y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }

then consider x being object such that

A2: [x,y] in A by XTUPLE_0:def 13;

ex x1, y1 being object st

( x1 in NAT & y1 in NAT & [x,y] = [x1,y1] ) by A2, ZFMISC_1:def 2;

then reconsider x = x, y = y as Element of NAT by XTUPLE_0:1;

( [x,y] in A & y is Element of NAT ) by A2;

hence y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ; :: thesis: verum

end;assume y in proj2 A ; :: thesis: y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }

then consider x being object such that

A2: [x,y] in A by XTUPLE_0:def 13;

ex x1, y1 being object st

( x1 in NAT & y1 in NAT & [x,y] = [x1,y1] ) by A2, ZFMISC_1:def 2;

then reconsider x = x, y = y as Element of NAT by XTUPLE_0:1;

( [x,y] in A & y is Element of NAT ) by A2;

hence y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ; :: thesis: verum

proof

hence
proj2 A = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
by A1; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } or y in proj2 A )

assume y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ; :: thesis: y in proj2 A

then ex y1 being Element of NAT st

( y = y1 & ex x being Element of NAT st [x,y1] in A ) ;

hence y in proj2 A by XTUPLE_0:def 13; :: thesis: verum

end;assume y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ; :: thesis: y in proj2 A

then ex y1 being Element of NAT st

( y = y1 & ex x being Element of NAT st [x,y1] in A ) ;

hence y in proj2 A by XTUPLE_0:def 13; :: thesis: verum