let X be set ; :: thesis: ( dom (id X) = X & rng (id X) = X )
thus dom (id X) = X :: thesis: rng (id X) = X

proof

now

let x be set ; :: thesis: ( x in X iff x in dom (id X) )

A1: now

assume x in dom (id X) ; :: thesis: x in X
then ex y being set st [x,y] in id X by Def4;
hence x in X by Def10; :: thesis: verum

end;

now

assume x in X ; :: thesis: x in dom (id X)
then [x,x] in id X by Def10;
hence x in dom (id X) by Def4; :: thesis: verum

end;

hence ( x in X iff x in dom (id X) ) by A1; :: thesis: verum

end;

hence dom (id X) = X by TARSKI:2; :: thesis: verum

end;

thus rng (id X) = X :: thesis: verum

proof

for x being set holds
( x in rng (id X) iff x in X )

proof

let x be set ; :: thesis: ( x in rng (id X) iff x in X )
thus ( x in rng (id X) implies x in X ) :: thesis: ( x in X implies x in rng (id X) )

proof

assume x in rng (id X) ; :: thesis: x in X
then consider y being set such that
A2: [y,x] in id X by Def5;
x = y by A2, Def10;
hence x in X by A2, Def10; :: thesis: verum

end;

( [x,x] in id X iff x in X ) by Def10;
hence ( x in X implies x in rng (id X) ) by Def5; :: thesis: verum

end;

hence rng (id X) = X by TARSKI:2; :: thesis: verum

end;