let X be set ; :: thesis: for Y being non empty set

for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

let Y be non empty set ; :: thesis: for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

let f be Function of X,Y; :: thesis: { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

set P = { (f " {y}) where y is Element of Y : y in rng f } ;

for x being object holds

( x in X iff ex A being set st

( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) )

A6: for A being Subset of X st A in { (f " {y}) where y is Element of Y : y in rng f } holds

( A <> {} & ( for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) )

for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

let Y be non empty set ; :: thesis: for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

let f be Function of X,Y; :: thesis: { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X

set P = { (f " {y}) where y is Element of Y : y in rng f } ;

for x being object holds

( x in X iff ex A being set st

( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) )

proof

then A5:
union { (f " {y}) where y is Element of Y : y in rng f } = X
by TARSKI:def 4;
let x be object ; :: thesis: ( x in X iff ex A being set st

( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) )

consider y being Element of Y such that

A4: ( f " {y} = A & y in rng f ) by A3;

thus x in X by A3, A4; :: thesis: verum

end;( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) )

hereby :: thesis: ( ex A being set st

( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) implies x in X )

given A being set such that A3:
( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )
; :: thesis: x in X( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) implies x in X )

assume A1:
x in X
; :: thesis: ex A being set st

( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )

then A2: ( f . x in rng f & f . x in Y ) by FUNCT_2:4, FUNCT_2:5;

reconsider A = f " {(f . x)} as set ;

take A = A; :: thesis: ( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )

f . x in {(f . x)} by TARSKI:def 1;

hence x in A by A1, FUNCT_2:38; :: thesis: A in { (f " {y}) where y is Element of Y : y in rng f }

thus A in { (f " {y}) where y is Element of Y : y in rng f } by A2; :: thesis: verum

end;( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )

then A2: ( f . x in rng f & f . x in Y ) by FUNCT_2:4, FUNCT_2:5;

reconsider A = f " {(f . x)} as set ;

take A = A; :: thesis: ( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )

f . x in {(f . x)} by TARSKI:def 1;

hence x in A by A1, FUNCT_2:38; :: thesis: A in { (f " {y}) where y is Element of Y : y in rng f }

thus A in { (f " {y}) where y is Element of Y : y in rng f } by A2; :: thesis: verum

consider y being Element of Y such that

A4: ( f " {y} = A & y in rng f ) by A3;

thus x in X by A3, A4; :: thesis: verum

A6: for A being Subset of X st A in { (f " {y}) where y is Element of Y : y in rng f } holds

( A <> {} & ( for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) )

proof

{ (f " {y}) where y is Element of Y : y in rng f } c= bool X
let A be Subset of X; :: thesis: ( A in { (f " {y}) where y is Element of Y : y in rng f } implies ( A <> {} & ( for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) ) )

assume A in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: ( A <> {} & ( for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) )

then consider y1 being Element of Y such that

A7: ( A = f " {y1} & y1 in rng f ) ;

consider x being object such that

A8: ( x in X & y1 = f . x ) by A7, FUNCT_2:11;

f . x in {y1} by A8, TARSKI:def 1;

hence A <> {} by A7, A8, FUNCT_2:38; :: thesis: for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B )

let B be Subset of X; :: thesis: ( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B )

assume B in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: ( A = B or A misses B )

then ex y2 being Element of Y st

( B = f " {y2} & y2 in rng f ) ;

hence ( A = B or A misses B ) by A7, ZFMISC_1:11, FUNCT_1:71; :: thesis: verum

end;( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) ) )

assume A in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: ( A <> {} & ( for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) )

then consider y1 being Element of Y such that

A7: ( A = f " {y1} & y1 in rng f ) ;

consider x being object such that

A8: ( x in X & y1 = f . x ) by A7, FUNCT_2:11;

f . x in {y1} by A8, TARSKI:def 1;

hence A <> {} by A7, A8, FUNCT_2:38; :: thesis: for B being Subset of X holds

( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B )

let B be Subset of X; :: thesis: ( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B )

assume B in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: ( A = B or A misses B )

then ex y2 being Element of Y st

( B = f " {y2} & y2 in rng f ) ;

hence ( A = B or A misses B ) by A7, ZFMISC_1:11, FUNCT_1:71; :: thesis: verum

proof

hence
{ (f " {y}) where y is Element of Y : y in rng f } is a_partition of X
by A5, A6, EQREL_1:def 4; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f " {y}) where y is Element of Y : y in rng f } or x in bool X )

assume x in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: x in bool X

then ex y being Element of Y st

( f " {y} = x & y in rng f ) ;

hence x in bool X ; :: thesis: verum

end;assume x in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: x in bool X

then ex y being Element of Y st

( f " {y} = x & y in rng f ) ;

hence x in bool X ; :: thesis: verum