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