:: by Unknown authors

::

:: Received Thu Mar 16 19:26:21 2017

:: Copyright Unknown

environ

vocabularies HIDDEN, CBS, SEQM_3, RELAT_1, XBOOLE_0, PARTFUN1, FUNCT_1, TARSKI, SUBSET_1, ZFMISC_1, RELAT_2, MCART_1, SETFAM_1, FUNCT_2, GROUP_9;

notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2;

definitions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1, FUNCT_2;

theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, PARTFUN1, GRFUNC_1, RELSET_1, SUBSET_1, XBOOLE_0, XBOOLE_1, RELAT_2, MCART_1, SETFAM_1, XTUPLE_0, FUNCT_2;

schemes FUNCT_1, PARTFUN1, XBOOLE_0, RELSET_1, SUBSET_1, FUNCT_2;

registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, GRFUNC_1, ZFMISC_1, FUNCT_2, FUNCOP_1;

constructors HIDDEN, RELAT_2, PARTFUN1, MCART_1, SETFAM_1, RELSET_1, XTUPLE_0, FUNCT_2;

requirements HIDDEN, SUBSET, BOOLE;

equalities PARTFUN1, SUBSET_1;

expansions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1, FUNCT_2;

definition

let A, B be set ;

let F be Function of (bool A),(bool B);

end;
let F be Function of (bool A),(bool B);

attr F is monotone means :DefMon: :: CBS4:def 1

for U, V being Subset of A st U c= V holds

F . U c= F . V;

for U, V being Subset of A st U c= V holds

F . U c= F . V;

attr F is anti-monotone means :DefAntiMon: :: CBS4:def 2

for U, V being Subset of A st U c= V holds

F . V c= F . U;

for U, V being Subset of A st U c= V holds

F . V c= F . U;

:: deftheorem DefMon defines monotone CBS4:def 1 :

for A, B being set

for F being Function of (bool A),(bool B) holds

( F is monotone iff for U, V being Subset of A st U c= V holds

F . U c= F . V );

for A, B being set

for F being Function of (bool A),(bool B) holds

( F is monotone iff for U, V being Subset of A st U c= V holds

F . U c= F . V );

:: deftheorem DefAntiMon defines anti-monotone CBS4:def 2 :

for A, B being set

for F being Function of (bool A),(bool B) holds

( F is anti-monotone iff for U, V being Subset of A st U c= V holds

F . V c= F . U );

for A, B being set

for F being Function of (bool A),(bool B) holds

( F is anti-monotone iff for U, V being Subset of A st U c= V holds

F . V c= F . U );

:: For sets $A$ and $B$ we

:: write $A\setminus B$ for $\{u\in A | u\notin B\}$.

:: JU: this is A \ B in Mizar:

:: write $A\setminus B$ for $\{u\in A | u\notin B\}$.

:: JU: this is A \ B in Mizar:

:: Let $A$ be a set and $\Phi:\wp(A)\to\wp(A)$ be

:: given by $\Phi(X)= A\setminus X$.

:: Then $\Phi$ is antimonotone.

:: given by $\Phi(X)= A\setminus X$.

:: Then $\Phi$ is antimonotone.

:: Let $f:A\to B$ be a function from a set $A$ to a set $B$.

:: For $X\in \wp(A)$ we write $f(X)$ for $\{f(x) | x\in X\}$.

:: JU: this is F " X or F .:X - lets test:

:: For $X\in \wp(A)$ we write $f(X)$ for $\{f(x) | x\in X\}$.

:: JU: this is F " X or F .:X - lets test:

:: Let $f:A\to B$ be a function from a set $A$ to a set $B$.

:: Let $\Phi:\wp(A)\to\wp(B)$ be given by $\Phi(X) = f(X)$.

:: Then $\Phi$ is monotone.

:: Let $\Phi:\wp(A)\to\wp(B)$ be given by $\Phi(X) = f(X)$.

:: Then $\Phi$ is monotone.

theorem TImMon: :: CBS4:4 :: ::[edit]

for A, B being set

for f being Function of A,B

for F being Function of (bool A),(bool B) st ( for U being Subset of A holds F . U = f .: U ) holds

F is monotone

for f being Function of A,B

for F being Function of (bool A),(bool B) st ( for U being Subset of A holds F . U = f .: U ) holds

F is monotone

proof

let A, B be set ; :: thesis: for f being Function of A,B

for F being Function of (bool A),(bool B) st ( for U being Subset of A holds F . U = f .: U ) holds

F is monotone

let f be Function of A,B; :: thesis: for F being Function of (bool A),(bool B) st ( for U being Subset of A holds F . U = f .: U ) holds

F is monotone

let F be Function of (bool A),(bool B); :: thesis: ( ( for U being Subset of A holds F . U = f .: U ) implies F is monotone )

assume A0: for U being Subset of A holds F . U = f .: U ; :: thesis: F is monotone

let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

F . U c= F . V

let V be Subset of A; :: thesis: ( U c= V implies F . U c= F . V )

assume A1: U c= V ; :: thesis: F . U c= F . V

A2: f .: U c= f .: V by RELAT_1:123, A1;

( F . V = f .: V & F . U = f .: U ) by A0;

hence F . U c= F . V by A2; :: thesis: verum

end;
for F being Function of (bool A),(bool B) st ( for U being Subset of A holds F . U = f .: U ) holds

F is monotone

let f be Function of A,B; :: thesis: for F being Function of (bool A),(bool B) st ( for U being Subset of A holds F . U = f .: U ) holds

F is monotone

let F be Function of (bool A),(bool B); :: thesis: ( ( for U being Subset of A holds F . U = f .: U ) implies F is monotone )

assume A0: for U being Subset of A holds F . U = f .: U ; :: thesis: F is monotone

let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

F . U c= F . V

let V be Subset of A; :: thesis: ( U c= V implies F . U c= F . V )

assume A1: U c= V ; :: thesis: F . U c= F . V

A2: f .: U c= f .: V by RELAT_1:123, A1;

( F . V = f .: V & F . U = f .: U ) by A0;

hence F . U c= F . V by A2; :: thesis: verum

theorem TAMonMon: :: CBS4:5 :: ::[edit]

for A, B, C being set

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C)

for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C)

for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

proof

let A, B, C be set ; :: thesis: for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C)

for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C)

for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

let G be Function of (bool B),(bool C); :: thesis: for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

let H be Function of (bool A),(bool C); :: thesis: ( F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) implies H is anti-monotone )

assume Z0: F is anti-monotone ; :: thesis: ( not G is monotone or ex U being Subset of A st not H . U = G . (F . U) or H is anti-monotone )

assume Z1: G is monotone ; :: thesis: ( ex U being Subset of A st not H . U = G . (F . U) or H is anti-monotone )

assume Z2: for U being Subset of A holds H . U = G . (F . U) ; :: thesis: H is anti-monotone

let U be Subset of A; :: according to CBS4:def 2 :: thesis: for V being Subset of A st U c= V holds

H . V c= H . U

let V be Subset of A; :: thesis: ( U c= V implies H . V c= H . U )

assume Z3: U c= V ; :: thesis: H . V c= H . U

Z4: F . V c= F . U by Z3, Z0;

then G . (F . V) c= G . (F . U) by Z1;

then H . V c= G . (F . U) by Z2;

hence H . V c= H . U by Z2; :: thesis: verum

end;
for G being Function of (bool B),(bool C)

for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C)

for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

let G be Function of (bool B),(bool C); :: thesis: for H being Function of (bool A),(bool C) st F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds

H is anti-monotone

let H be Function of (bool A),(bool C); :: thesis: ( F is anti-monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) implies H is anti-monotone )

assume Z0: F is anti-monotone ; :: thesis: ( not G is monotone or ex U being Subset of A st not H . U = G . (F . U) or H is anti-monotone )

assume Z1: G is monotone ; :: thesis: ( ex U being Subset of A st not H . U = G . (F . U) or H is anti-monotone )

assume Z2: for U being Subset of A holds H . U = G . (F . U) ; :: thesis: H is anti-monotone

let U be Subset of A; :: according to CBS4:def 2 :: thesis: for V being Subset of A st U c= V holds

H . V c= H . U

let V be Subset of A; :: thesis: ( U c= V implies H . V c= H . U )

assume Z3: U c= V ; :: thesis: H . V c= H . U

Z4: F . V c= F . U by Z3, Z0;

then G . (F . V) c= G . (F . U) by Z1;

then H . V c= G . (F . U) by Z2;

hence H . V c= H . U by Z2; :: thesis: verum

theorem TMonMon1: :: CBS4:8 :: ::[edit]

for A, B, C being set

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is monotone & G is monotone holds

G * F is monotone

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is monotone & G is monotone holds

G * F is monotone

proof

let A, B, C be set ; :: thesis: for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is monotone & G is monotone holds

G * F is monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C) st F is monotone & G is monotone holds

G * F is monotone

let G be Function of (bool B),(bool C); :: thesis: ( F is monotone & G is monotone implies G * F is monotone )

assume Z4: F is monotone ; :: thesis: ( not G is monotone or G * F is monotone )

assume Z5: G is monotone ; :: thesis: G * F is monotone

let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

(G * F) . U c= (G * F) . V

let V be Subset of A; :: thesis: ( U c= V implies (G * F) . U c= (G * F) . V )

assume Z6: U c= V ; :: thesis: (G * F) . U c= (G * F) . V

Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;

(G * F) . V = G . (F . V) by FUNCT_2:15;

hence (G * F) . U c= (G * F) . V by Z7, Z5, Z6, Z4; :: thesis: verum

end;
for G being Function of (bool B),(bool C) st F is monotone & G is monotone holds

G * F is monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C) st F is monotone & G is monotone holds

G * F is monotone

let G be Function of (bool B),(bool C); :: thesis: ( F is monotone & G is monotone implies G * F is monotone )

assume Z4: F is monotone ; :: thesis: ( not G is monotone or G * F is monotone )

assume Z5: G is monotone ; :: thesis: G * F is monotone

let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

(G * F) . U c= (G * F) . V

let V be Subset of A; :: thesis: ( U c= V implies (G * F) . U c= (G * F) . V )

assume Z6: U c= V ; :: thesis: (G * F) . U c= (G * F) . V

Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;

(G * F) . V = G . (F . V) by FUNCT_2:15;

hence (G * F) . U c= (G * F) . V by Z7, Z5, Z6, Z4; :: thesis: verum

registration

let A, B be set ;

ex b_{1} being Function of (bool A),(bool B) st

( b_{1} is monotone & b_{1} is anti-monotone )

end;
cluster Relation-like bool A -defined bool B -valued Function-like non empty total quasi_total monotone anti-monotone for Element of bool [:(bool A),(bool B):];

existence ex b

( b

proof

consider F being constant Function of (bool A),(bool B) such that

verum ;

take F ; :: thesis: ( F is monotone & F is anti-monotone )

thus F is monotone :: thesis: F is anti-monotone

F . V c= F . U

let V be Subset of A; :: thesis: ( U c= V implies F . V c= F . U )

assume A1: U c= V ; :: thesis: F . V c= F . U

( U in bool A & V in bool A ) ;

then ( U in dom F & V in dom F ) by FUNCT_2:def 1;

then F . U = F . V by FUNCT_1:def 10;

hence F . V c= F . U ; :: thesis: verum

end;
verum ;

take F ; :: thesis: ( F is monotone & F is anti-monotone )

thus F is monotone :: thesis: F is anti-monotone

proof

let U be Subset of A; :: according to CBS4:def 2 :: thesis: for V being Subset of A st U c= V holds
let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

F . U c= F . V

let V be Subset of A; :: thesis: ( U c= V implies F . U c= F . V )

assume A1: U c= V ; :: thesis: F . U c= F . V

( U in bool A & V in bool A ) ;

then ( U in dom F & V in dom F ) by FUNCT_2:def 1;

then F . U = F . V by FUNCT_1:def 10;

hence F . U c= F . V ; :: thesis: verum

end;
F . U c= F . V

let V be Subset of A; :: thesis: ( U c= V implies F . U c= F . V )

assume A1: U c= V ; :: thesis: F . U c= F . V

( U in bool A & V in bool A ) ;

then ( U in dom F & V in dom F ) by FUNCT_2:def 1;

then F . U = F . V by FUNCT_1:def 10;

hence F . U c= F . V ; :: thesis: verum

F . V c= F . U

let V be Subset of A; :: thesis: ( U c= V implies F . V c= F . U )

assume A1: U c= V ; :: thesis: F . V c= F . U

( U in bool A & V in bool A ) ;

then ( U in dom F & V in dom F ) by FUNCT_2:def 1;

then F . U = F . V by FUNCT_1:def 10;

hence F . V c= F . U ; :: thesis: verum

registration

let A, B, C be set ;

let F be monotone Function of (bool A),(bool B);

let G be monotone Function of (bool B),(bool C);

correctness

coherence

for b_{1} being Function of (bool A),(bool C) st b_{1} = G * F holds

b_{1} is monotone ;

by TMonMon1;

end;
let F be monotone Function of (bool A),(bool B);

let G be monotone Function of (bool B),(bool C);

correctness

coherence

for b

b

by TMonMon1;

theorem TAMonAMon1: :: CBS4:9 :: ::[edit]

for A, B, C being set

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is anti-monotone & G is anti-monotone holds

G * F is monotone

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is anti-monotone & G is anti-monotone holds

G * F is monotone

proof

let A, B, C be set ; :: thesis: for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is anti-monotone & G is anti-monotone holds

G * F is monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C) st F is anti-monotone & G is anti-monotone holds

G * F is monotone

let G be Function of (bool B),(bool C); :: thesis: ( F is anti-monotone & G is anti-monotone implies G * F is monotone )

assume Z4: F is anti-monotone ; :: thesis: ( not G is anti-monotone or G * F is monotone )

assume Z5: G is anti-monotone ; :: thesis: G * F is monotone

let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

(G * F) . U c= (G * F) . V

let V be Subset of A; :: thesis: ( U c= V implies (G * F) . U c= (G * F) . V )

assume Z6: U c= V ; :: thesis: (G * F) . U c= (G * F) . V

Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;

(G * F) . V = G . (F . V) by FUNCT_2:15;

hence (G * F) . U c= (G * F) . V by Z7, Z5, Z6, Z4; :: thesis: verum

end;
for G being Function of (bool B),(bool C) st F is anti-monotone & G is anti-monotone holds

G * F is monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C) st F is anti-monotone & G is anti-monotone holds

G * F is monotone

let G be Function of (bool B),(bool C); :: thesis: ( F is anti-monotone & G is anti-monotone implies G * F is monotone )

assume Z4: F is anti-monotone ; :: thesis: ( not G is anti-monotone or G * F is monotone )

assume Z5: G is anti-monotone ; :: thesis: G * F is monotone

let U be Subset of A; :: according to CBS4:def 1 :: thesis: for V being Subset of A st U c= V holds

(G * F) . U c= (G * F) . V

let V be Subset of A; :: thesis: ( U c= V implies (G * F) . U c= (G * F) . V )

assume Z6: U c= V ; :: thesis: (G * F) . U c= (G * F) . V

Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;

(G * F) . V = G . (F . V) by FUNCT_2:15;

hence (G * F) . U c= (G * F) . V by Z7, Z5, Z6, Z4; :: thesis: verum

registration

let A, B, C be set ;

let F be anti-monotone Function of (bool A),(bool B);

let G be anti-monotone Function of (bool B),(bool C);

correctness

coherence

for b_{1} being Function of (bool A),(bool C) st b_{1} = G * F holds

b_{1} is monotone ;

by TAMonAMon1;

end;
let F be anti-monotone Function of (bool A),(bool B);

let G be anti-monotone Function of (bool B),(bool C);

correctness

coherence

for b

b

by TAMonAMon1;

theorem TAMonMon1: :: CBS4:10 :: ::[edit]

for A, B, C being set

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is anti-monotone & G is monotone holds

G * F is anti-monotone

for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is anti-monotone & G is monotone holds

G * F is anti-monotone

proof

let A, B, C be set ; :: thesis: for F being Function of (bool A),(bool B)

for G being Function of (bool B),(bool C) st F is anti-monotone & G is monotone holds

G * F is anti-monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C) st F is anti-monotone & G is monotone holds

G * F is anti-monotone

let G be Function of (bool B),(bool C); :: thesis: ( F is anti-monotone & G is monotone implies G * F is anti-monotone )

assume Z4: F is anti-monotone ; :: thesis: ( not G is monotone or G * F is anti-monotone )

assume Z5: G is monotone ; :: thesis: G * F is anti-monotone

let U be Subset of A; :: according to CBS4:def 2 :: thesis: for V being Subset of A st U c= V holds

(G * F) . V c= (G * F) . U

let V be Subset of A; :: thesis: ( U c= V implies (G * F) . V c= (G * F) . U )

assume Z6: U c= V ; :: thesis: (G * F) . V c= (G * F) . U

Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;

(G * F) . V = G . (F . V) by FUNCT_2:15;

hence (G * F) . V c= (G * F) . U by Z7, Z5, Z6, Z4; :: thesis: verum

end;
for G being Function of (bool B),(bool C) st F is anti-monotone & G is monotone holds

G * F is anti-monotone

let F be Function of (bool A),(bool B); :: thesis: for G being Function of (bool B),(bool C) st F is anti-monotone & G is monotone holds

G * F is anti-monotone

let G be Function of (bool B),(bool C); :: thesis: ( F is anti-monotone & G is monotone implies G * F is anti-monotone )

assume Z4: F is anti-monotone ; :: thesis: ( not G is monotone or G * F is anti-monotone )

assume Z5: G is monotone ; :: thesis: G * F is anti-monotone

let U be Subset of A; :: according to CBS4:def 2 :: thesis: for V being Subset of A st U c= V holds

(G * F) . V c= (G * F) . U

let V be Subset of A; :: thesis: ( U c= V implies (G * F) . V c= (G * F) . U )

assume Z6: U c= V ; :: thesis: (G * F) . V c= (G * F) . U

Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;

(G * F) . V = G . (F . V) by FUNCT_2:15;

hence (G * F) . V c= (G * F) . U by Z7, Z5, Z6, Z4; :: thesis: verum

registration

let A, B, C be set ;

let F be anti-monotone Function of (bool A),(bool B);

let G be monotone Function of (bool B),(bool C);

correctness

coherence

for b_{1} being Function of (bool A),(bool C) st b_{1} = G * F holds

b_{1} is anti-monotone ;

by TAMonMon1;

end;
let F be anti-monotone Function of (bool A),(bool B);

let G be monotone Function of (bool B),(bool C);

correctness

coherence

for b

b

by TAMonMon1;

:: Knaster-Tarski theorem

:: Let $\Phi:\wp(A)\to\wp(A)$.

:: Assume $\Phi$ is monotone.

:: Then there is some $Y\in\wp(A)$ such that $\Phi(Y)=Y$.

:: Let $\Phi:\wp(A)\to\wp(A)$.

:: Assume $\Phi$ is monotone.

:: Then there is some $Y\in\wp(A)$ such that $\Phi(Y)=Y$.

theorem TKnasterTarski: :: CBS4:11 :: ::[edit]

for A being set

for F being Function of (bool A),(bool A) st F is monotone holds

ex U being Subset of A st F . U = U

for F being Function of (bool A),(bool A) st F is monotone holds

ex U being Subset of A st F . U = U

proof

let A be set ; :: thesis: for F being Function of (bool A),(bool A) st F is monotone holds

ex U being Subset of A st F . U = U

let F be Function of (bool A),(bool A); :: thesis: ( F is monotone implies ex U being Subset of A st F . U = U )

assume A0: F is monotone ; :: thesis: ex U being Subset of A st F . U = U

set Y0 = { U where U is Subset of A : F . U c= U } ;

B0: not { U where U is Subset of A : F . U c= U } is empty

set Y = meet Y1;

meet Y1 is Subset of A ;

take meet Y1 ; :: thesis: F . (meet Y1) = meet Y1

A1: for U being Subset of A st F . U c= U holds

meet Y1 c= U

end;
ex U being Subset of A st F . U = U

let F be Function of (bool A),(bool A); :: thesis: ( F is monotone implies ex U being Subset of A st F . U = U )

assume A0: F is monotone ; :: thesis: ex U being Subset of A st F . U = U

set Y0 = { U where U is Subset of A : F . U c= U } ;

B0: not { U where U is Subset of A : F . U c= U } is empty

proof

{ U where U is Subset of A : F . U c= U } c= bool A
F . ([#] A) c= A
;

then [#] A in { U where U is Subset of A : F . U c= U } ;

hence not { U where U is Subset of A : F . U c= U } is empty ; :: thesis: verum

end;
then [#] A in { U where U is Subset of A : F . U c= U } ;

hence not { U where U is Subset of A : F . U c= U } is empty ; :: thesis: verum

proof

then reconsider Y1 = { U where U is Subset of A : F . U c= U } as Subset-Family of A by B0;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { U where U is Subset of A : F . U c= U } or u in bool A )

assume Z1: u in { U where U is Subset of A : F . U c= U } ; :: thesis: u in bool A

consider U being Subset of A such that

Z2: ( U = u & F . U c= U ) by Z1;

U in bool A ;

hence u in bool A by B0, Z2; :: thesis: verum

end;
assume Z1: u in { U where U is Subset of A : F . U c= U } ; :: thesis: u in bool A

consider U being Subset of A such that

Z2: ( U = u & F . U c= U ) by Z1;

U in bool A ;

hence u in bool A by B0, Z2; :: thesis: verum

set Y = meet Y1;

meet Y1 is Subset of A ;

take meet Y1 ; :: thesis: F . (meet Y1) = meet Y1

A1: for U being Subset of A st F . U c= U holds

meet Y1 c= U

proof

thus A2:
F . (meet Y1) c= meet Y1
:: according to XBOOLE_0:def 10 :: thesis: meet Y1 c= F . (meet Y1)
let U be Subset of A; :: thesis: ( F . U c= U implies meet Y1 c= U )

assume Z1: F . U c= U ; :: thesis: meet Y1 c= U

then U in { U where U is Subset of A : F . U c= U } ;

hence meet Y1 c= U by SETFAM_1:3; :: thesis: verum

end;
assume Z1: F . U c= U ; :: thesis: meet Y1 c= U

then U in { U where U is Subset of A : F . U c= U } ;

hence meet Y1 c= U by SETFAM_1:3; :: thesis: verum

proof

thus
meet Y1 c= F . (meet Y1)
:: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in F . (meet Y1) or z in meet Y1 )

assume B1: z in F . (meet Y1) ; :: thesis: z in meet Y1

for u being set st u in { U where U is Subset of A : F . U c= U } holds

z in u

hence z in meet Y1 ; :: thesis: verum

end;
assume B1: z in F . (meet Y1) ; :: thesis: z in meet Y1

for u being set st u in { U where U is Subset of A : F . U c= U } holds

z in u

proof

then
z in meet { U where U is Subset of A : F . U c= U }
by B0, SETFAM_1:def 1;
let u be set ; :: thesis: ( u in { U where U is Subset of A : F . U c= U } implies z in u )

assume Z2: u in { U where U is Subset of A : F . U c= U } ; :: thesis: z in u

consider U being Subset of A such that

Z3: u = U and

Z4: F . U c= U by Z2;

meet Y1 c= U by A1, Z4;

then F . (meet Y1) c= F . U by A0, DefMon;

hence z in u by B1, Z3, Z4, TARSKI:def 3; :: thesis: verum

end;
assume Z2: u in { U where U is Subset of A : F . U c= U } ; :: thesis: z in u

consider U being Subset of A such that

Z3: u = U and

Z4: F . U c= U by Z2;

meet Y1 c= U by A1, Z4;

then F . (meet Y1) c= F . U by A0, DefMon;

hence z in u by B1, Z3, Z4, TARSKI:def 3; :: thesis: verum

hence z in meet Y1 ; :: thesis: verum

:: Let $f:A\to B$ be a function.

:: We say $f$ is {\em{injective}} if $\forall xy\in A. f(x) = f(y) \to x = y$.

:: JU: this is one-to-one in Mizar:

:: for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2;

:: We say $f$ is {\em{injective}} if $\forall xy\in A. f(x) = f(y) \to x = y$.

:: JU: this is one-to-one in Mizar:

:: for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2;

:: We say sets $A$ and $B$ are {\em{equipotent}} if there exists a relation $R$ such that

:: \item $\forall x\in A.\exists y\in B. (x,y)\in R$

:: \item $\forall y\in B.\exists x\in A. (x,y)\in R$

:: \item $\forall x\in A.\forall y\in B.\forall z\in A.\forall w\in B.(x,y)\in R \land (z,w)\in R \to (x=z \iff y=w)$

:: \item $\forall x\in A.\exists y\in B. (x,y)\in R$

:: \item $\forall y\in B.\exists x\in A. (x,y)\in R$

:: \item $\forall x\in A.\forall y\in B.\forall z\in A.\forall w\in B.(x,y)\in R \land (z,w)\in R \to (x=z \iff y=w)$

:: this is by KNASTER:12; too bad, let's ignore KNASTER

:: If $f:A\to B$ and $g:B\to A$ are injective,

:: then $A$ and $B$ are equipotent.

:: If $f:A\to B$ and $g:B\to A$ are injective,

:: then $A$ and $B$ are equipotent.

theorem TCBS: :: CBS4:14 :: ::[edit]

for A, B being non empty set

for f being Function of A,B

for g being Function of B,A st f is one-to-one & g is one-to-one holds

A,B are_equipotent

for f being Function of A,B

for g being Function of B,A st f is one-to-one & g is one-to-one holds

A,B are_equipotent

proof

let A, B be non empty set ; :: thesis: for f being Function of A,B

for g being Function of B,A st f is one-to-one & g is one-to-one holds

A,B are_equipotent

let f be Function of A,B; :: thesis: for g being Function of B,A st f is one-to-one & g is one-to-one holds

A,B are_equipotent

let g be Function of B,A; :: thesis: ( f is one-to-one & g is one-to-one implies A,B are_equipotent )

assume A0: ( f is one-to-one & g is one-to-one ) ; :: thesis: A,B are_equipotent

deffunc H_{1}( Subset of A) -> Element of bool A = g .: (B \ (f .: (A \ $1)));

consider F being Function of (bool A),(bool A) such that

A1: for U being Subset of A holds F . U = H_{1}(U)
from FUNCT_2:sch 4();

A2: F is monotone

A3: F . C = C by TKnasterTarski, A2;

A4: C c= A ;

A5: for x being object holds

( x in C iff x in g .: (B \ (f .: (A \ C))) ) by A1, A3;

set R = { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ;

take { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ; :: according to TARSKI:def 6 :: thesis: ( ( for b_{1} being object holds

( not b_{1} in A or ex b_{2} being object st

( b_{2} in B & [b_{1},b_{2}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) ) ) & ( for b_{1} being object holds

( not b_{1} in B or ex b_{2} being object st

( b_{2} in A & [b_{2},b_{1}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } or not [b_{3},b_{4}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) ) ) )

thus for x being object st x in A holds

ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) :: thesis: ( ( for b_{1} being object holds

( not b_{1} in B or ex b_{2} being object st

( b_{2} in A & [b_{2},b_{1}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } or not [b_{3},b_{4}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) ) ) )

ex x being object st

( x in A & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) ; :: thesis: for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } or not [b_{3},b_{4}] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) )

A6: for x, y being object st x in A & y in B & x in C & x = g . y holds

not y in f .: (A \ C) ;

thus for x, y, z, u being object st [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } & [z,u] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } holds

( x = z iff y = u ) ; :: thesis: verum

end;
for g being Function of B,A st f is one-to-one & g is one-to-one holds

A,B are_equipotent

let f be Function of A,B; :: thesis: for g being Function of B,A st f is one-to-one & g is one-to-one holds

A,B are_equipotent

let g be Function of B,A; :: thesis: ( f is one-to-one & g is one-to-one implies A,B are_equipotent )

assume A0: ( f is one-to-one & g is one-to-one ) ; :: thesis: A,B are_equipotent

deffunc H

consider F being Function of (bool A),(bool A) such that

A1: for U being Subset of A holds F . U = H

A2: F is monotone

proof

consider C being Subset of A such that
deffunc H_{2}( Subset of A) -> Element of bool A = A \ $1;

deffunc H_{3}( Subset of A) -> Element of bool B = f .: $1;

deffunc H_{4}( Subset of B) -> Element of bool B = B \ $1;

deffunc H_{5}( Subset of B) -> Element of bool A = g .: $1;

consider G1 being Function of (bool A),(bool A) such that

B1: for U being Subset of A holds G1 . U = H_{2}(U)
from FUNCT_2:sch 4();

consider G2 being Function of (bool A),(bool B) such that

B2: for U being Subset of A holds G2 . U = H_{3}(U)
from FUNCT_2:sch 4();

consider G3 being Function of (bool B),(bool B) such that

B3: for W being Subset of B holds G3 . W = H_{4}(W)
from FUNCT_2:sch 4();

consider G4 being Function of (bool B),(bool A) such that

B4: for W being Subset of B holds G4 . W = H_{5}(W)
from FUNCT_2:sch 4();

B5: for U being Subset of A holds H_{1}(U) = H_{5}(H_{4}(H_{3}(H_{2}(U))))
;

B6: for u being object st u in bool A holds

( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u )

C1: G1 is anti-monotone by TSetMinusAntimon, B1;

C2: G2 is monotone by TImMon, B2;

C3: G3 is anti-monotone by TSetMinusAntimon, B3;

C4: G4 is monotone by TImMon, B4;

hence F is monotone by B7, C1, C2, C3, C4; :: thesis: verum

end;
deffunc H

deffunc H

deffunc H

consider G1 being Function of (bool A),(bool A) such that

B1: for U being Subset of A holds G1 . U = H

consider G2 being Function of (bool A),(bool B) such that

B2: for U being Subset of A holds G2 . U = H

consider G3 being Function of (bool B),(bool B) such that

B3: for W being Subset of B holds G3 . W = H

consider G4 being Function of (bool B),(bool A) such that

B4: for W being Subset of B holds G4 . W = H

B5: for U being Subset of A holds H

B6: for u being object st u in bool A holds

( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u )

proof

then B7:
F = G4 * (G3 * (G2 * G1))
by FUNCT_2:15, FUNCT_2:12;
let u be object ; :: thesis: ( u in bool A implies ( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u ) )

assume D1: u in bool A ; :: thesis: ( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u )

reconsider U = u as Element of bool A by D1;

D2: F . U = H_{1}(U)
by A1

.= H_{5}(H_{4}(H_{3}(H_{2}(U))))

.= H_{5}(H_{4}(H_{3}(G1 . U)))
by B1

.= H_{5}(H_{4}(G2 . (G1 . U)))
by B2

.= H_{5}(G3 . (G2 . (G1 . U)))
by B3

.= G4 . (G3 . (G2 . (G1 . U))) by B4 ;

G2 . (G1 . U) = (G2 * G1) . U by FUNCT_2:15;

then G3 . (G2 . (G1 . U)) = (G3 * (G2 * G1)) . U by FUNCT_2:15;

then G4 . (G3 . (G2 . (G1 . U))) = (G4 * (G3 * (G2 * G1))) . U by FUNCT_2:15;

hence ( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u ) by D2, FUNCT_2:15; :: thesis: verum

end;
assume D1: u in bool A ; :: thesis: ( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u )

reconsider U = u as Element of bool A by D1;

D2: F . U = H

.= H

.= H

.= H

.= H

.= G4 . (G3 . (G2 . (G1 . U))) by B4 ;

G2 . (G1 . U) = (G2 * G1) . U by FUNCT_2:15;

then G3 . (G2 . (G1 . U)) = (G3 * (G2 * G1)) . U by FUNCT_2:15;

then G4 . (G3 . (G2 . (G1 . U))) = (G4 * (G3 * (G2 * G1))) . U by FUNCT_2:15;

hence ( F . u = G4 . (G3 . (G2 . (G1 . u))) & F . u = (G4 * (G3 * (G2 * G1))) . u ) by D2, FUNCT_2:15; :: thesis: verum

C1: G1 is anti-monotone by TSetMinusAntimon, B1;

C2: G2 is monotone by TImMon, B2;

C3: G3 is anti-monotone by TSetMinusAntimon, B3;

C4: G4 is monotone by TImMon, B4;

hence F is monotone by B7, C1, C2, C3, C4; :: thesis: verum

A3: F . C = C by TKnasterTarski, A2;

A4: C c= A ;

A5: for x being object holds

( x in C iff x in g .: (B \ (f .: (A \ C))) ) by A1, A3;

set R = { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ;

take { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ; :: according to TARSKI:def 6 :: thesis: ( ( for b

( not b

( b

( not b

( b

( not [b

thus for x being object st x in A holds

ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) :: thesis: ( ( for b

( not b

( b

( not [b

proof

thus
for y being object st y in B holds
let x be object ; :: thesis: ( x in A implies ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) )

assume B0: x in A ; :: thesis: ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

reconsider x1 = x as Element of A by B0;

end;
( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) )

assume B0: x in A ; :: thesis: ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

reconsider x1 = x as Element of A by B0;

per cases
( not x1 in C or x1 in C )
;

end;

suppose B1:
not x1 in C
; :: thesis: ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

take y = f . x1; :: thesis: ( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

thus y in B ; :: thesis: [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) }

thus [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } by B1; :: thesis: verum

end;
thus y in B ; :: thesis: [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) }

thus [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } by B1; :: thesis: verum

suppose B2:
x1 in C
; :: thesis: ex y being object st

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

then
x1 in g .: (B \ (f .: (A \ C)))
by A5;

then consider y being object such that

B3: ( y in B & y in B \ (f .: (A \ C)) & x1 = g . y ) by FUNCT_2:64, A5, B2;

take y ; :: thesis: ( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

thus y in B by B3; :: thesis: [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) }

thus [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } by B2, B3; :: thesis: verum

end;
then consider y being object such that

B3: ( y in B & y in B \ (f .: (A \ C)) & x1 = g . y ) by FUNCT_2:64, A5, B2;

take y ; :: thesis: ( y in B & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } )

thus y in B by B3; :: thesis: [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) }

thus [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } by B2, B3; :: thesis: verum

ex x being object st

( x in A & [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } ) ; :: thesis: for b

( not [b

A6: for x, y being object st x in A & y in B & x in C & x = g . y holds

not y in f .: (A \ C) ;

thus for x, y, z, u being object st [x,y] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } & [z,u] in { [x,y] where x is Element of A, y is Element of B : ( ( not x in C & y = f . x ) or ( x in C & x = g . y ) ) } holds

( x = z iff y = u ) ; :: thesis: verum

:: If $f:A\to B$ is injective and $B\subseteq A$,

:: then $A$ and $B$ are equipotent.

:: then $A$ and $B$ are equipotent.

theorem TCor1: :: CBS4:15 :: ::[edit]

for A, B being non empty set

for f being Function of A,B st f is one-to-one & B c= A holds

A,B are_equipotent ;

for f being Function of A,B st f is one-to-one & B c= A holds

A,B are_equipotent ;

:: $\Phi(U)\subseteq \Phi(V)$ forall $U,V\in\wp(A)$ such that $U\subseteq V$.

:: We say $\Phi$ is {\em{antimonotone}} if

:: $\Phi(V)\subseteq \Phi(U)$ forall $U,V\in\wp(A)$ such that $U\subseteq V$.