:: We present a proof of Cantor-Bernstein-Schr\"oder based on Knaster's argument in~\cite{Knaster1928}. The proof is given at a level of detail sufficient to prepare the reader to consider corresponding formal proofs in interactive theorem provers.
:: by Unknown authors
::
:: Received Thu Mar 16 18:50:23 2017

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;

:: Let $\Phi:\wp(A)\to\wp(B)$. We say $\Phi$ is {\em{monotone}} if
:: $\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$.
definition
let A, B be set ;
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;
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;
end;

:: 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 );

:: 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 sets $A$ and $B$ we
:: write $A\setminus B$ for $\{u\in A | u\notin B\}$.
:: JU: this is A \ B in Mizar:
theorem :: CBS4:1
for A, B being set holds A \ B = A \ B ;

:: Let $A$ be a set and $\Phi:\wp(A)\to\wp(A)$ be
:: given by $\Phi(X)= A\setminus X$.
:: Then $\Phi$ is antimonotone.
theorem TSetMinusAntimon: :: CBS4:2
for A being set
for F being Function of (bool A),(bool A) st ( for U being Subset of A holds F . U = A \ U ) holds
F is anti-monotone ;

:: 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:
theorem :: CBS4:3
for A, B being set
for F being Function of (bool A),(bool B)
for U being Subset of A holds F .: U = F .: U ;

:: 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.
theorem TImMon: :: CBS4:4
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
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 ;
( F . V = f .: V & F . U = f .: U ) by A0;
hence F . U c= F . V by A2; :: thesis: verum
end;

theorem TAMonMon: :: CBS4:5
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
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:
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;

theorem TAMonAMon: :: CBS4:6
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 anti-monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds
H is monotone ;

theorem TMonMon: :: CBS4:7
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 monotone & G is monotone & ( for U being Subset of A holds H . U = G . (F . U) ) holds
H is monotone ;

theorem TMonMon1: :: CBS4:8
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
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;

registration
let A, B be set ;
existence
ex b1 being Function of (bool A),(bool B) st
( b1 is monotone & b1 is anti-monotone )
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:
proof
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;
let U be Subset of A; :: according to CBS4:def 2 :: thesis: for V being Subset of A st U c= V holds
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;
end;

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);
cluster F * G -> monotone for Function of (bool A),(bool C);
correctness
coherence
for b1 being Function of (bool A),(bool C) st b1 = G * F holds
b1 is monotone
;
by TMonMon1;
end;

theorem TAMonAMon1: :: CBS4:9
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
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;

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);
cluster F * G -> monotone for Function of (bool A),(bool C);
correctness
coherence
for b1 being Function of (bool A),(bool C) st b1 = G * F holds
b1 is monotone
;
by TAMonAMon1;
end;

theorem TAMonMon1: :: CBS4:10
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
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;

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);
cluster F * G -> anti-monotone for Function of (bool A),(bool C);
correctness
coherence
for b1 being Function of (bool A),(bool C) st b1 = G * F holds
b1 is anti-monotone
;
by TAMonMon1;
end;

:: 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$.
theorem TKnasterTarski: :: CBS4:11
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
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
proof
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;
{ U where U is Subset of A : F . U c= U } c= bool A
proof
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;
then reconsider Y1 = { U where U is Subset of A : F . U c= U } as Subset-Family of A by B0;
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
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;
thus A2: F . (meet Y1) c= meet Y1 :: according to XBOOLE_0:def 10 :: thesis: meet Y1 c= F . (meet Y1)
proof
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
proof
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 ;
hence z in u by ; :: thesis: verum
end;
then z in meet { U where U is Subset of A : F . U c= U } by ;
hence z in meet Y1 ; :: thesis: verum
end;
thus meet Y1 c= F . (meet Y1) :: thesis: verum
proof
F . (F . (meet Y1)) c= F . (meet Y1) by ;
hence meet Y1 c= F . (meet Y1) by A1; :: thesis: verum
end;
end;

:: 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;
theorem ThInj: :: CBS4:12
for A, B being non empty set
for f being Function of A,B holds
( f is one-to-one iff for x, y being object st x in A & y in A & f . x = f . y holds
x = y ) by FUNCT_2:19;

:: 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)$
theorem :: CBS4:13
for A, B being non empty set holds
( A,B are_equipotent iff A,B are_equipotent ) ;

:: 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.
theorem TCBS: :: CBS4:14
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
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:
deffunc H1( 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 = H1(U) from A2: F is monotone proof deffunc H2( Subset of A) -> Element of bool A = A \$1;
deffunc H3( Subset of A) -> Element of bool B = f .: $1; deffunc H4( Subset of B) -> Element of bool B = B \$1;
deffunc H5( 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 = H2(U) from consider G2 being Function of (bool A),(bool B) such that B2: for U being Subset of A holds G2 . U = H3(U) from consider G3 being Function of (bool B),(bool B) such that B3: for W being Subset of B holds G3 . W = H4(W) from consider G4 being Function of (bool B),(bool A) such that B4: for W being Subset of B holds G4 . W = H5(W) from B5: for U being Subset of A holds H1(U) = H5(H4(H3(H2(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 ) proof 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 = H1(U) by A1 .= H5(H4(H3(H2(U)))) .= H5(H4(H3(G1 . U))) by B1 .= H5(H4(G2 . (G1 . U))) by B2 .= H5(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 ; :: thesis: verum end; then B7: F = G4 * (G3 * (G2 * G1)) by ; C1: G1 is anti-monotone by ; C2: G2 is monotone by ; C3: G3 is anti-monotone by ; C4: G4 is monotone by ; hence F is monotone by B7, C1, C2, C3, C4; :: thesis: verum end; consider C being Subset of A such that A3: F . C = C by ; 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 b1 being object holds ( not b1 in A or ex b2 being object st ( b2 in B & [b1,b2] 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 b1 being object holds ( not b1 in B or ex b2 being object st ( b2 in A & [b2,b1] 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 b1, b2, b3, b4 being object holds ( not [b1,b2] 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 [b3,b4] 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 b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) ) 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 b1 being object holds ( not b1 in B or ex b2 being object st ( b2 in A & [b2,b1] 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 b1, b2, b3, b4 being object holds ( not [b1,b2] 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 [b3,b4] 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 b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) ) proof 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; per cases ( not x1 in C or x1 in C ) ; 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 ) ) } ) 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; 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 ) ) } ) 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 ; 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; end; end; thus for y being object st y in B holds 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 b1, b2, b3, b4 being object holds ( not [b1,b2] 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 [b3,b4] 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 b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) 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; :: If$f:A\to B$is injective and$B\subseteq A$, :: then$A$and$B\$ are equipotent.
theorem TCor1: :: CBS4:15
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 ;