let U be Grothendieck; :: thesis: for f being Function st dom f in U & rng f c= U holds

rng f in U

let f be Function; :: thesis: ( dom f in U & rng f c= U implies rng f in U )

assume A1: ( dom f in U & rng f c= U ) ; :: thesis: rng f in U

set A = dom f;

A2: ( U is epsilon-transitive & U is power-closed & U is FamUnion-closed ) ;

deffunc H_{1}( set ) -> set = {(f . $1)};

consider s being Function such that

A3: ( dom s = dom f & ( for X being set st X in dom f holds

s . X = H_{1}(X) ) )
from FUNCT_1:sch 5();

rng s c= U

A7: Union s c= rng f

hence rng f in U by CARD_3:def 4, A6; :: thesis: verum

rng f in U

let f be Function; :: thesis: ( dom f in U & rng f c= U implies rng f in U )

assume A1: ( dom f in U & rng f c= U ) ; :: thesis: rng f in U

set A = dom f;

A2: ( U is epsilon-transitive & U is power-closed & U is FamUnion-closed ) ;

deffunc H

consider s being Function such that

A3: ( dom s = dom f & ( for X being set st X in dom f holds

s . X = H

rng s c= U

proof

then A6:
union (rng s) in U
by A3, A1, A2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in U )

assume y in rng s ; :: thesis: y in U

then consider x being object such that

A4: ( x in dom s & s . x = y ) by FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

f . x in rng f by A4, A3, FUNCT_1:def 3;

then bool (f . x) in U by A1, A2;

then A5: bool (bool (f . x)) c= U by A2;

H_{1}(x) c= bool (f . x)
by ZFMISC_1:68;

then H_{1}(x) in bool (bool (f . x))
;

then y in bool (bool (f . x)) by A4, A3;

hence y in U by A5; :: thesis: verum

end;assume y in rng s ; :: thesis: y in U

then consider x being object such that

A4: ( x in dom s & s . x = y ) by FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

f . x in rng f by A4, A3, FUNCT_1:def 3;

then bool (f . x) in U by A1, A2;

then A5: bool (bool (f . x)) c= U by A2;

H

then H

then y in bool (bool (f . x)) by A4, A3;

hence y in U by A5; :: thesis: verum

A7: Union s c= rng f

proof

rng f c= Union s
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union s or y in rng f )

assume y in Union s ; :: thesis: y in rng f

then consider x being object such that

A8: ( x in dom s & y in s . x ) by CARD_5:2;

reconsider x = x as set by TARSKI:1;

s . x = H_{1}(x)
by A8, A3;

then y = f . x by A8, TARSKI:def 1;

hence y in rng f by A8, A3, FUNCT_1:def 3; :: thesis: verum

end;assume y in Union s ; :: thesis: y in rng f

then consider x being object such that

A8: ( x in dom s & y in s . x ) by CARD_5:2;

reconsider x = x as set by TARSKI:1;

s . x = H

then y = f . x by A8, TARSKI:def 1;

hence y in rng f by A8, A3, FUNCT_1:def 3; :: thesis: verum

proof

then
rng f = Union s
by A7;
let fx be object ; :: according to TARSKI:def 3 :: thesis: ( not fx in rng f or fx in Union s )

assume fx in rng f ; :: thesis: fx in Union s

then consider x being object such that

A9: ( x in dom f & f . x = fx ) by FUNCT_1:def 3;

reconsider x = x as set by A9;

( fx in H_{1}(x) & H_{1}(x) = s . x )
by A9, A3, TARSKI:def 1;

hence fx in Union s by A9, A3, CARD_5:2; :: thesis: verum

end;assume fx in rng f ; :: thesis: fx in Union s

then consider x being object such that

A9: ( x in dom f & f . x = fx ) by FUNCT_1:def 3;

reconsider x = x as set by A9;

( fx in H

hence fx in Union s by A9, A3, CARD_5:2; :: thesis: verum

hence rng f in U by CARD_3:def 4, A6; :: thesis: verum