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

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

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

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

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

proof

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

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

then consider y being object such that

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

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 x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ; :: thesis: verum

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

then consider y being object such that

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

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 x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ; :: thesis: verum

proof

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

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

then ex x1 being Element of NAT st

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

hence x in proj1 A by XTUPLE_0:def 12; :: thesis: verum

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

then ex x1 being Element of NAT st

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

hence x in proj1 A by XTUPLE_0:def 12; :: thesis: verum