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


:: 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 ::Show TPTP problem ::[edit]
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 ::Show TPTP problem ::[edit]
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 ::Show TPTP problem ::[edit]
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 ::Show TPTP problem ::[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
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;

theorem TAMonMon: :: CBS4:5 ::Show TPTP problem ::[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
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;

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

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

theorem TMonMon1: :: CBS4:8 ::Show TPTP problem ::[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
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 ;
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 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: F is anti-monotone
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 ::Show TPTP problem ::[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
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 ::Show TPTP problem ::[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
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;

:: WP: 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 ::Show TPTP problem ::[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
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 A0, DefMon;
hence z in u by B1, Z3, Z4, TARSKI:def 3; :: thesis: verum
end;
then z in meet { U where U is Subset of A : F . U c= U } by B0, SETFAM_1:def 1;
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 A2, A0, DefMon;
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 ::Show TPTP problem ::[edit]
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 ::Show TPTP problem ::[edit]
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 ::Show TPTP problem ::[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
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 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 FUNCT_2:sch 4();
 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 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 = H3(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 = H4(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 = H5(W) from FUNCT_2:sch 4();
 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 D2, FUNCT_2:15; :: thesis: verum
end;
then B7: F = G4 * (G3 * (G2 * G1)) by FUNCT_2:15, FUNCT_2:12;
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;
consider C being Subset of A such that
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 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 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;
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 ::Show TPTP problem ::[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 ;