let X be set ; :: thesis: for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent

let F be Subset-Family of X; :: thesis: F, COMPLEMENT F are_equipotent

deffunc H_{1}( set ) -> Element of bool X = X \ $1;

consider f being Function such that

A1: dom f = F and

A2: for x being set st x in F holds

f . x = H_{1}(x)
from FUNCT_1:sch 5();

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = F & rng f = COMPLEMENT F )

thus f is one-to-one :: thesis: ( dom f = F & rng f = COMPLEMENT F )

thus rng f c= COMPLEMENT F :: according to XBOOLE_0:def 10 :: thesis: COMPLEMENT F c= rng f

assume A8: e in COMPLEMENT F ; :: thesis: e in rng f

then reconsider Y = e as Subset of X ;

A9: Y ` in F by A8, SETFAM_1:def 7;

e = (Y `) `

.= f . (Y `) by A2, A9 ;

hence e in rng f by A1, A9, FUNCT_1:def 3; :: thesis: verum

let F be Subset-Family of X; :: thesis: F, COMPLEMENT F are_equipotent

deffunc H

consider f being Function such that

A1: dom f = F and

A2: for x being set st x in F holds

f . x = H

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = F & rng f = COMPLEMENT F )

thus f is one-to-one :: thesis: ( dom f = F & rng f = COMPLEMENT F )

proof

thus
dom f = F
by A1; :: thesis: rng f = COMPLEMENT F
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A3: x1 in dom f and

A4: x2 in dom f and

A5: f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4;

X1 ` = f . x1 by A1, A2, A3

.= X2 ` by A1, A2, A4, A5 ;

hence x1 = (X2 `) `

.= x2 ;

:: thesis: verum

end;assume that

A3: x1 in dom f and

A4: x2 in dom f and

A5: f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4;

X1 ` = f . x1 by A1, A2, A3

.= X2 ` by A1, A2, A4, A5 ;

hence x1 = (X2 `) `

.= x2 ;

:: thesis: verum

thus rng f c= COMPLEMENT F :: according to XBOOLE_0:def 10 :: thesis: COMPLEMENT F c= rng f

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in COMPLEMENT F or e in rng f )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng f or e in COMPLEMENT F )

assume e in rng f ; :: thesis: e in COMPLEMENT F

then consider u being object such that

A6: u in dom f and

A7: e = f . u by FUNCT_1:def 3;

reconsider Y = u as Subset of X by A1, A6;

e = Y ` by A1, A2, A6, A7;

hence e in COMPLEMENT F by A1, A6, SETFAM_1:35; :: thesis: verum

end;assume e in rng f ; :: thesis: e in COMPLEMENT F

then consider u being object such that

A6: u in dom f and

A7: e = f . u by FUNCT_1:def 3;

reconsider Y = u as Subset of X by A1, A6;

e = Y ` by A1, A2, A6, A7;

hence e in COMPLEMENT F by A1, A6, SETFAM_1:35; :: thesis: verum

assume A8: e in COMPLEMENT F ; :: thesis: e in rng f

then reconsider Y = e as Subset of X ;

A9: Y ` in F by A8, SETFAM_1:def 7;

e = (Y `) `

.= f . (Y `) by A2, A9 ;

hence e in rng f by A1, A9, FUNCT_1:def 3; :: thesis: verum