:: K\"onig's Theorem
:: by Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDINAL1, CARD_1, SUBSET_1, FUNCT_1, RELAT_1, FUNCOP_1, XBOOLE_0,
ZFMISC_1, TARSKI, FUNCT_2, MCART_1, FINSET_1, NAT_1, WELLORD1, WELLORD2,
RELAT_2, SETFAM_1, PARTFUN1, FUNCT_4, CARD_3, PBOOLE, NAGATA_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, RELAT_1,
RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, ORDINAL1,
WELLORD1, MCART_1, WELLORD2, FUNCOP_1, FUNCT_4, FINSET_1, FINSUB_1,
PBOOLE;
constructors SETFAM_1, RELAT_2, WELLORD1, PARTFUN1, WELLORD2, FUNCOP_1,
FUNCT_4, CLASSES1, ORDINAL2, ORDINAL3, FINSET_1, CARD_1, FINSUB_1,
RELSET_1, FUNCT_1, PBOOLE, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FUNCT_4,
FINSET_1, CARD_1, PBOOLE, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, RELAT_2, WELLORD1, WELLORD2, XBOOLE_0, RELAT_1,
ORDINAL1, PARTFUN1;
equalities XBOOLE_0, FUNCOP_1, RELAT_1, ORDINAL1;
expansions TARSKI, FUNCT_1, RELAT_2, WELLORD1, WELLORD2, XBOOLE_0, RELAT_1,
ORDINAL1, PARTFUN1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, MCART_1, ORDINAL1, RELAT_1,
WELLORD1, WELLORD2, CARD_1, FUNCOP_1, FUNCT_5, GRFUNC_1, XBOOLE_0,
XBOOLE_1, SETFAM_1, FUNCT_4, PARTFUN1, RELSET_1, SUBSET_1, FINSET_1,
XTUPLE_0;
schemes FUNCT_1, PARTFUN1, ORDINAL1, FUNCT_5, RELAT_1, XBOOLE_0, CLASSES1,
XFAMILY;
begin
reserve A,B,C for Ordinal,
K,L,M,N for Cardinal,
x,y,y1,y2,z,u for object,X,Y,Z,Z1,Z2 for set,
n for Nat,
f,f1,g,h for Function,
Q,R for Relation;
definition
let IT be Function;
attr IT is Cardinal-yielding means
:Def1: for x st x in dom IT holds IT.x is Cardinal;
end;
registration
cluster empty -> Cardinal-yielding for Function;
coherence;
end;
registration
cluster Cardinal-yielding for Function;
existence
proof
take {};
thus thesis;
end;
end;
definition
mode Cardinal-Function is Cardinal-yielding Function;
end;
reserve ff for Cardinal-Function;
registration
let ff,X;
cluster ff|X -> Cardinal-yielding;
coherence
proof
ff|X is Cardinal-yielding
proof
let x;
assume
A1: x in dom(ff|X);
then
A2: (ff|X).x = ff.x by FUNCT_1:47;
dom(ff|X) = dom ff /\ X by RELAT_1:61;
then x in dom ff by A1,XBOOLE_0:def 4;
hence thesis by A2,Def1;
end;
hence thesis;
end;
end;
registration
let X,K;
cluster X --> K -> Cardinal-yielding;
coherence by FUNCOP_1:7;
end;
registration
let X be object; let K;
cluster X .--> K -> Cardinal-yielding;
coherence;
end;
scheme CFLambda { A()->set, F(object)->Cardinal } :
ex ff st dom ff = A() & for x being set st x in A() holds ff.x = F(x)
proof
consider f such that
A1: dom f = A() & for x being object st x in A()
holds f.x = F(x) from FUNCT_1:sch 3;
f is Cardinal-yielding
proof
let x;
assume x in dom f;
then f.x = F(x) by A1;
hence thesis;
end;
then reconsider f as Cardinal-Function;
take f;
thus thesis by A1;
end;
definition
let f;
func Card f -> Cardinal-Function means
:
Def2: dom it = dom f & for x st x in dom f holds it.x = card(f.x);
existence
proof
deffunc f(object) = card (f.$1);
consider g being Cardinal-Function such that
A1: dom g = dom f and
A2: for x being set st x in dom f holds g.x = f(x) from CFLambda;
take g;
thus dom g = dom f by A1;
let x be object such that
A3: x in dom f;
reconsider x as set by TARSKI:1;
g.x = f(x) by A3,A2;
hence thesis;
end;
uniqueness
proof
let a1,a2 be Cardinal-Function such that
A4: dom a1 = dom f and
A5: for x st x in dom f holds a1.x = card(f.x) and
A6: dom a2 = dom f and
A7: for x st x in dom f holds a2.x = card(f.x);
now
let x be object;
assume
A8: x in dom f;
then a1.x = card(f.x) by A5;
hence a1.x = a2.x by A7,A8;
end;
hence thesis by A4,A6;
end;
func disjoin f -> Function means
:
Def3: dom it = dom f &
for x being object st x in dom f holds it.x = [:f.x,{x}:];
existence
proof
deffunc f(object) = [:f.$1,{$1}:];
thus ex g being Function st
dom g = dom f &
for x being object st x in dom f holds g.x = f(x) from FUNCT_1:sch 3;
end;
uniqueness
proof
let a1,a2 be Function such that
A9: dom a1 = dom f and
A10: for x being object st x in dom f holds a1.x = [:f.x,{x}:] and
A11: dom a2 = dom f and
A12: for x being object st x in dom f holds a2.x = [:f.x,{x}:];
now
let x be object;
assume
A13: x in dom f;
then a1.x = [:f.x,{x}:] by A10;
hence a1.x = a2.x by A12,A13;
end;
hence thesis by A9,A11;
end;
func Union f -> set equals
union rng f;
correctness;
defpred P[object] means
ex g st $1 = g & dom g = dom f &
for x being object st x in dom f holds g.x in f.x;
func product f -> set means
:Def5: for x being object holds x in it iff ex g st x = g & dom g = dom f &
for y being object st y in dom f holds g.y in f.y;
existence
proof
consider X such that
A14: for x being object holds
x in X iff x in Funcs(dom f, union rng f) & P[x] from XBOOLE_0:sch 1;
take X;
let x be object;
thus x in X implies ex g st x = g & dom g = dom f &
for x being object st x in dom f holds g.x in f.x by A14;
given g such that
A15: x = g and
A16: dom g = dom f and
A17: for x being object st x in dom f holds g.x in f.x;
rng g c= union rng f
proof
let y be object;
assume y in rng g;
then consider z being object such that
A18: z in dom g and
A19: y = g.z by FUNCT_1:def 3;
A20: y in f.z by A16,A17,A18,A19;
f.z in rng f by A16,A18,FUNCT_1:def 3;
hence thesis by A20,TARSKI:def 4;
end;
then x in Funcs(dom f, union rng f) by A15,A16,FUNCT_2:def 2;
hence thesis by A14,A15,A16,A17;
end;
uniqueness
proof
let X1,X2 be set such that
A21: for x being object holds x in X1 iff P[x] and
A22: for x being object holds x in X2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A21,A22);
end;
end;
theorem Th1:
Card ff = ff
proof
now
let x;
assume x in dom ff;
then reconsider M = ff.x as Cardinal by Def1;
card M = M;
hence ff.x = card (ff.x);
end;
hence thesis by Def2;
end;
theorem
Card (X --> Y) = X --> card Y
proof
A1: dom Card (X --> Y) = dom(X --> Y) by Def2;
then
A2: dom Card (X --> Y) = X;
now
let x be object;
assume
A4: x in X;
then
A5: Card (X --> Y).x = card ((X --> Y).x) by A1,Def2;
(X --> card Y).x = card Y by A4,FUNCOP_1:7;
hence Card (X --> Y).x = (X --> card Y).x by A4,A5,FUNCOP_1:7;
end;
hence thesis by A2;
end;
theorem
disjoin {} = {}
by Def3,RELAT_1:38;
theorem Th4:
disjoin (x .--> X) = x .--> [:X,{x}:]
proof
A1: dom disjoin ({x} --> X) = dom ({x} --> X) by Def3;
A2: dom ({x} --> X) = {x};
now
let y be object;
assume
A4: y in {x};
then
A5: disjoin ({x} --> X).y = [:({x} --> X).y,{y}:] by A2,Def3;
A6: ({x} --> X).y = X by A4,FUNCOP_1:7;
({x} --> [:X,{x}:]).y = [:X,{x}:] by A4,FUNCOP_1:7;
hence disjoin ({x} --> X).y = ({x} --> [:X,{x}:]).y by A4,A5,A6,
TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem
x in dom f & y in dom f & x <> y implies (disjoin f).x misses (disjoin f).y
proof
assume that
A1: x in dom f and
A2: y in dom f and
A3: x <> y;
set z = the Element of ((disjoin f).x) /\ ((disjoin f).y);
assume
A4: ((disjoin f).x) /\ ((disjoin f).y) <> {};
A5: (disjoin f).x = [:f.x,{x}:] by A1,Def3;
A6: (disjoin f).y = [:f.y,{y}:] by A2,Def3;
A7: z in (disjoin f).x by A4,XBOOLE_0:def 4;
A8: z in (disjoin f).y by A4,XBOOLE_0:def 4;
A9: z`2 in {x} by A5,A7,MCART_1:10;
A10: z`2 in {y} by A6,A8,MCART_1:10;
z`2 = x by A9,TARSKI:def 1;
hence contradiction by A3,A10,TARSKI:def 1;
end;
theorem Th6:
Union (X --> Y) c= Y
proof
let x be object;
assume x in Union (X --> Y);
then consider Z such that
A1: x in Z and
A2: Z in rng (X --> Y) by TARSKI:def 4;
ex z being object st z in dom (X --> Y) & Z = (X --> Y).z
by A2,FUNCT_1:def 3;
hence thesis by A1,FUNCOP_1:7;
end;
theorem Th7:
X <> {} implies Union (X --> Y) = Y
proof
assume
A1: X <> {};
set x = the Element of X;
thus Union (X --> Y) c= Y by Th6;
A2: dom (X --> Y) = X;
(X --> Y).x = Y by A1,FUNCOP_1:7;
then Y in rng (X --> Y) by A1,A2,FUNCT_1:def 3;
hence thesis by ZFMISC_1:74;
end;
theorem
Union (x .--> Y) = Y by Th7;
theorem Th9:
g in product f iff dom g = dom f &
for x being object st x in dom f holds g.x in f.x
proof
thus g in product f implies
dom g = dom f & for x being object st x in dom f holds g.x in f.x
proof
assume g in product f;
then ex h being Function st
g = h & dom h = dom f &
for x being object st x in dom f holds h.x in f.x by Def5;
hence thesis;
end;
thus thesis by Def5;
end;
theorem Th10:
product {} = {{}}
proof
thus product {} c= {{}}
proof
let x be object;
assume x in product {};
then ex g st
x = g & dom g = dom {} &
for y being object st y in dom {} holds g.y in {} .y by Def5;
then x = {};
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {{}};
then
A1: x = {} by TARSKI:def 1;
for y being object st y in dom {} holds {} .y in {} .y;
hence thesis by A1,Th9;
end;
theorem Th11:
Funcs(X,Y) = product (X --> Y)
proof
set f = (X --> Y);
thus Funcs(X,Y) c= product f
proof
let x be object;
assume x in Funcs(X,Y);
then consider g such that
A2: x = g and
A3: dom g = X and
A4: rng g c= Y by FUNCT_2:def 2;
now
let y be object;
assume
A5: y in dom f;
then
A6: f.y = Y by FUNCOP_1:7;
g.y in rng g by A3,A5,FUNCT_1:def 3;
hence g.y in f.y by A4,A6;
end;
hence thesis by A2,A3,Def5;
end;
let x be object;
assume x in product f;
then consider g such that
A7: x = g and
A8: dom g = dom f and
A9: for x being object st x in dom f holds g.x in f.x by Def5;
rng g c= Y
proof
let y be object;
assume y in rng g;
then consider z being object such that
A10: z in dom g and
A11: y = g.z by FUNCT_1:def 3;
y in f.z by A8,A9,A10,A11;
hence thesis by A8,A10,FUNCOP_1:7;
end;
hence thesis by A7,A8,FUNCT_2:def 2;
end;
defpred P[object] means $1 is Function;
definition
let x be object; let X;
defpred R[object,object] means ex g st $1 = g & $2 = g.x;
func pi(X,x) -> set means
: Def6:
for y being object holds y in it iff ex f st f in X & y = f.x;
existence
proof
consider Y such that
A1: for y being object holds y in Y iff y in X & P[y] from XBOOLE_0:sch 1;
A2: for y being object st y in Y ex z being object st R[y,z]
proof
let y be object;
assume y in Y;
then reconsider y as Function by A1;
take y.x, y;
thus thesis;
end;
consider f such that
A3: dom f = Y &
for y being object st y in Y holds R[y,f.y] from CLASSES1:sch 1(A2);
take rng f;
let y be object;
thus y in rng f implies ex f st f in X & y = f.x
proof
assume y in rng f;
then consider z being object such that
A4: z in dom f and
A5: y = f.z by FUNCT_1:def 3;
consider g such that
A6: z = g and
A7: f.z = g.x by A3,A4;
take g;
thus thesis by A1,A3,A4,A5,A6,A7;
end;
given g such that
A8: g in X and
A9: y = g.x;
A10: g in Y by A1,A8;
then ex f1 st g = f1 & f.g = f1.x by A3;
hence thesis by A3,A9,A10,FUNCT_1:def 3;
end;
uniqueness
proof
defpred Z[object] means ex f st f in X & $1 = f.x;
let X1,X2 be set such that
A11: for y being object holds y in X1 iff Z[y] and
A12: for y being object holds y in X2 iff Z[y];
thus thesis from XBOOLE_0:sch 2(A11,A12);
end;
end;
theorem
x in dom f & product f <> {} implies pi(product f,x) = f.x
proof
assume that
A1: x in dom f and
A2: product f <> {};
A3: pi(product f,x) c= f.x
proof
let y be object;
assume y in pi(product f,x);
then ex g st g in product f & y = g.x by Def6;
hence thesis by A1,Th9;
end;
f.x c= pi(product f,x)
proof set z = the Element of product f;
consider g such that
z = g and
A4: dom g = dom f and
A5: for x being object st x in dom f holds g.x in f.x by A2,Def5;
let y be object;
reconsider yy=y as set by TARSKI:1;
deffunc f(object) = yy;
deffunc g(object) = g.$1;
defpred C[object] means x = $1;
consider h being Function such that
A6: dom h = dom g & for z being object st z in dom g holds
(C[z] implies h.z = f(z)) & (not C[z] implies h.z = g(z)) from
PARTFUN1:sch 1;
assume
A7: y in f.x;
now
let z be object;
assume
A8: z in dom f;
then x <> z implies g.z = h.z by A4,A6;
hence h.z in f.z by A4,A5,A6,A7,A8;
end;
then
A9: h in product f by A4,A6,Th9;
h.x = y by A1,A4,A6;
hence thesis by A9,Def6;
end;
hence thesis by A3;
end;
theorem
pi({},x) = {}
proof
set y = the Element of pi({},x);
assume not thesis;
then ex f st f in {} & y = f.x by Def6;
hence contradiction;
end;
theorem
pi({g},x) = {g.x}
proof
thus pi({g},x) c= {g.x}
proof
let y be object;
assume y in pi({g},x);
then consider f such that
A1: f in {g} and
A2: y = f.x by Def6;
f = g by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
let y be object;
assume
A3: y in {g.x};
A4: g in {g} by TARSKI:def 1;
y = g.x by A3,TARSKI:def 1;
hence thesis by A4,Def6;
end;
theorem
pi({f,g},x) = {f.x,g.x}
proof
thus pi({f,g},x) c= {f.x,g.x}
proof
let y be object;
assume y in pi({f,g},x);
then consider f1 such that
A1: f1 in {f,g} and
A2: y = f1.x by Def6;
f1 = f or f1 = g by A1,TARSKI:def 2;
hence thesis by A2,TARSKI:def 2;
end;
let y be object;
assume
A3: y in {f.x,g.x};
A4: f in {f,g} by TARSKI:def 2;
A5: g in {f,g} by TARSKI:def 2;
y = g.x or y = f.x by A3,TARSKI:def 2;
hence thesis by A4,A5,Def6;
end;
theorem Th16:
pi(X \/ Y,x) = pi(X,x) \/ pi(Y,x)
proof
thus pi(X \/ Y,x) c= pi(X,x) \/ pi(Y,x)
proof
let y be object;
assume y in pi(X \/ Y,x);
then consider f such that
A1: f in X \/ Y and
A2: y = f.x by Def6;
f in X or f in Y by A1,XBOOLE_0:def 3;
then y in pi(X,x) or y in pi(Y,x) by A2,Def6;
hence thesis by XBOOLE_0:def 3;
end;
let y be object;
assume y in pi(X,x) \/ pi(Y,x);
then
A3: y in pi(X,x) or y in pi(Y,x) by XBOOLE_0:def 3;
A4: now
assume y in pi(X,x);
then consider f such that
A5: f in X and
A6: y = f.x by Def6;
f in X \/ Y by A5,XBOOLE_0:def 3;
hence thesis by A6,Def6;
end;
now
assume not y in pi(X,x);
then consider f such that
A7: f in Y and
A8: y = f.x by A3,Def6;
f in X \/ Y by A7,XBOOLE_0:def 3;
hence thesis by A8,Def6;
end;
hence thesis by A4;
end;
theorem
pi(X /\ Y,x) c= pi(X,x) /\ pi(Y,x)
proof
let y be object;
assume y in pi(X /\ Y,x);
then consider f such that
A1: f in X /\ Y and
A2: y = f.x by Def6;
A3: f in X by A1,XBOOLE_0:def 4;
A4: f in Y by A1,XBOOLE_0:def 4;
A5: y in pi(X,x) by A2,A3,Def6;
y in pi(Y,x) by A2,A4,Def6;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th18:
pi(X,x) \ pi(Y,x) c= pi(X \ Y,x)
proof
let y be object;
assume
A1: y in pi(X,x) \ pi(Y,x);
then consider f such that
A2: f in X and
A3: y = f.x by Def6;
not y in pi(Y,x) by A1,XBOOLE_0:def 5;
then not f in Y by A3,Def6;
then f in X \ Y by A2,XBOOLE_0:def 5;
hence thesis by A3,Def6;
end;
theorem
pi(X,x) \+\ pi(Y,x) c= pi(X \+\ Y,x)
proof
A1: pi(X,x) \ pi(Y,x) c= pi(X\Y,x) by Th18;
A2: pi(Y,x) \ pi(X,x) c= pi(Y\X,x) by Th18;
pi(X\Y,x) \/ pi(Y\X,x) = pi((X\Y) \/ (Y\X),x) by Th16;
hence thesis by A1,A2,XBOOLE_1:13;
end;
theorem Th20:
card pi(X,x) c= card X
proof
consider Y such that
A1: for y being object holds y in Y iff y in X & P[y] from XBOOLE_0:sch 1;
defpred R[object,object] means ex g st $1 = g & $2 = g.x;
A2: for y being object st y in Y ex z being object st R[y,z]
proof
let y be object;
assume y in Y;
then reconsider y as Function by A1;
take y.x, y;
thus thesis;
end;
consider f such that
A3: dom f = Y &
for y being object st y in Y holds R[y,f.y] from CLASSES1:sch 1(A2);
now
let y be object;
thus y in rng f implies ex f st f in X & y = f.x
proof
assume y in rng f;
then consider z being object such that
A4: z in dom f and
A5: y = f.z by FUNCT_1:def 3;
consider g such that
A6: z = g and
A7: f.z = g.x by A3,A4;
take g;
thus thesis by A1,A3,A4,A5,A6,A7;
end;
given g such that
A8: g in X and
A9: y = g.x;
A10: g in Y by A1,A8;
then ex f1 st g = f1 & f.g = f1.x by A3;
hence y in rng f by A3,A9,A10,FUNCT_1:def 3;
end;
then rng f = pi(X,x) by Def6;
then
A11: card pi(X,x) c= card Y by A3,CARD_1:12;
Y c= X
by A1;
then card Y c= card X by CARD_1:11;
hence thesis by A11;
end;
theorem Th21:
x in Union disjoin f implies ex y,z being object st x = [y,z]
proof
assume x in Union disjoin f;
then consider X such that
A1: x in X and
A2: X in rng disjoin f by TARSKI:def 4;
consider y being object such that
A3: y in dom disjoin f and
A4: X = (disjoin f).y by A2,FUNCT_1:def 3;
y in dom f by A3,Def3;
then X = [:f.y,{y}:] by A4,Def3;
hence thesis by A1,RELAT_1:def 1;
end;
theorem Th22:
x in Union disjoin f iff x`2 in dom f & x`1 in f.(x`2) & x = [x`1,x`2]
proof
thus x in Union disjoin f implies
x`2 in dom f & x`1 in f.(x`2) & x = [x`1,x`2]
proof
assume x in Union disjoin f;
then consider X such that
A1: x in X and
A2: X in rng disjoin f by TARSKI:def 4;
consider y being object such that
A3: y in dom disjoin f and
A4: X = (disjoin f).y by A2,FUNCT_1:def 3;
A5: y in dom f by A3,Def3;
then
A6: X = [:f.y,{y}:] by A4,Def3;
then
A7: x`1 in f.y by A1,MCART_1:10;
x`2 in {y} by A1,A6,MCART_1:10;
hence thesis by A1,A5,A6,A7,MCART_1:21,TARSKI:def 1;
end;
assume that
A8: x`2 in dom f and
A9: x`1 in f.(x`2) and
A10: x = [x`1,x`2];
A11: (disjoin f).(x`2) = [:f.(x`2),{x`2}:] by A8,Def3;
A12: dom f = dom disjoin f by Def3;
x`2 in {x`2} by TARSKI:def 1;
then
A13: x in [:f.(x`2),{x`2}:] by A9,A10,ZFMISC_1:87;
[:f.(x`2),{x`2}:] in rng disjoin f by A8,A11,A12,FUNCT_1:def 3;
hence thesis by A13,TARSKI:def 4;
end;
theorem Th23:
f c= g implies disjoin f c= disjoin g
proof
assume
A1: f c= g;
then
A2: dom f c= dom g by GRFUNC_1:2;
A3: dom disjoin f = dom f by Def3;
A4: dom disjoin g = dom g by Def3;
now
let x be object;
assume
A5: x in dom disjoin f;
then
A6: (disjoin f).x = [:f.x,{x}:] by A3,Def3;
f.x = g.x by A1,A3,A5,GRFUNC_1:2;
hence (disjoin f).x = (disjoin g).x by A2,A3,A5,A6,Def3;
end;
hence thesis by A2,A3,A4,GRFUNC_1:2;
end;
theorem Th24:
f c= g implies Union f c= Union g
proof
assume
A1: f c= g;
then
A2: dom f c= dom g by GRFUNC_1:2;
let x be object;
assume x in Union f;
then consider X such that
A3: x in X and
A4: X in rng f by TARSKI:def 4;
consider y being object such that
A5: y in dom f and
A6: X = f.y by A4,FUNCT_1:def 3;
f.y = g.y by A1,A5,GRFUNC_1:2;
then X in rng g by A2,A5,A6,FUNCT_1:def 3;
hence thesis by A3,TARSKI:def 4;
end;
theorem
Union disjoin (Y --> X) = [:X,Y:]
proof
set f = Y --> X;
A1: dom f = Y;
thus Union disjoin f c= [:X,Y:]
proof
let x be object;
assume x in Union disjoin f;
then consider Z such that
A2: x in Z and
A3: Z in rng disjoin f by TARSKI:def 4;
consider y being object such that
A4: y in dom disjoin f and
A5: Z = (disjoin f).y by A3,FUNCT_1:def 3;
A6: y in Y by A1,A4,Def3;
then
A7: Z = [:f.y,{y}:] by A1,A5,Def3;
A8: f.y = X by A6,FUNCOP_1:7;
{y} c= Y by A6,ZFMISC_1:31;
then Z c= [:X,Y:] by A7,A8,ZFMISC_1:95;
hence thesis by A2;
end;
let x1,x2 be object;
assume
A9: [x1,x2] in [:X,Y:];
then
A10: x1 in X by ZFMISC_1:87;
A11: x2 in Y by A9,ZFMISC_1:87;
then
A12: f.x2 = X by FUNCOP_1:7;
A13: (disjoin f).(x2) = [:f.x2,{x2}:] by A1,A11,Def3;
A14: x2 in dom disjoin f by A1,A11,Def3;
x2 in {x2} by TARSKI:def 1;
then
A15: [x1,x2] in [:f.x2,{x2}:] by A10,A12,ZFMISC_1:87;
[:f.x2,{x2}:] in rng disjoin f by A13,A14,FUNCT_1:def 3;
hence thesis by A15,TARSKI:def 4;
end;
theorem Th26:
product f = {} iff {} in rng f
proof
thus product f = {} implies {} in rng f
proof
assume that
A1: product f = {} and
A2: not {} in rng f;
A3: now
assume dom f = {};
then for x being object st x in dom f holds f.x in f.x;
hence thesis by A1,Def5;
end;
now
assume dom f <> {};
then reconsider M = rng f as non empty set by RELAT_1:42;
X in M implies X <> {} by A2;
then consider f1 such that
dom f1 = M and
A4: for X st X in M holds f1.X in X by FUNCT_1:111;
deffunc g(object) = f1.(f.$1);
consider g such that
A5: dom
g = dom f &
for x being object st x in dom f holds g.x = g(x) from FUNCT_1:sch 3;
now
let x be object;
assume
A6: x in dom f;
then
A7: f.x in M by FUNCT_1:def 3;
g.x = f1.(f.x) by A5,A6;
hence g.x in f.x by A4,A7;
end;
hence thesis by A1,A5,Def5;
end;
hence thesis by A3;
end;
assume {} in rng f;
then
A8: ex x being object st x in dom f & {} = f.x by FUNCT_1:def 3;
assume
A9: product f <> {};
set y = the Element of product f;
ex g st ( y = g)&( dom g = dom f)&( for x being object st x in dom f
holds g.x in f.x) by A9,Def5;
hence contradiction by A8;
end;
theorem Th27:
dom f = dom g & (for x st x in dom f holds f.x c= g.x) implies
product f c= product g
proof
assume that
A1: dom f = dom g and
A2: for x st x in dom f holds f.x c= g.x;
let x be object;
assume x in product f;
then consider f1 such that
A3: x = f1 and
A4: dom f1 = dom f and
A5: for x being object st x in dom f holds f1.x in f.x by Def5;
now
let x be object;
assume
A6: x in dom g;
then
A7: f1.x in f.x by A1,A5;
f.x c= g.x by A1,A2,A6;
hence f1.x in g.x by A7;
end;
hence thesis by A1,A3,A4,Def5;
end;
reserve F,G for Cardinal-Function;
theorem
for x st x in dom F holds card (F.x) = F.x
proof
let x;
assume x in dom F;
then reconsider M = F.x as Cardinal by Def1;
card M = M;
hence thesis;
end;
theorem Th29:
for x st x in dom F holds card ((disjoin F).x) = F.x
proof
let x;
assume
A1: x in dom F;
then reconsider M = F.x as Cardinal by Def1;
M,[:M,{x}:] are_equipotent by CARD_1:69;
then M = card [:M,{x}:] by CARD_1:def 2;
hence thesis by A1,Def3;
end;
definition
let F;
func Sum F -> Cardinal equals
card Union disjoin F;
correctness;
func Product F -> Cardinal equals
card product F;
correctness;
end;
theorem
dom F = dom G & (for x st x in dom F holds F.x c= G.x) implies Sum F c= Sum
G
proof
assume that
A1: dom F = dom G and
A2: for x st x in dom F holds F.x c= G.x;
Union disjoin F c= Union disjoin G
proof
let x be object;
assume x in Union disjoin F;
then consider X such that
A3: x in X and
A4: X in rng disjoin F by TARSKI:def 4;
consider y being object such that
A5: y in dom disjoin F and
A6: X = (disjoin F).y by A4,FUNCT_1:def 3;
A7: y in dom F by A5,Def3;
then
A8: F.y c= G.y by A2;
A9: X = [:F.y,{y}:] by A6,A7,Def3;
A10: (disjoin G).y = [:G.y,{y}:] by A1,A7,Def3;
A11: y in dom disjoin G by A1,A7,Def3;
A12: X c= [:G.y,{y}:] by A8,A9,ZFMISC_1:95;
[:G.y,{y}:] in rng disjoin G by A10,A11,FUNCT_1:def 3;
hence thesis by A3,A12,TARSKI:def 4;
end;
hence thesis by CARD_1:11;
end;
theorem
{} in rng F iff Product F = 0
proof
thus {} in rng F implies Product F = 0 by Th26,CARD_1:27;
assume Product F = 0;
then product F = {};
hence thesis by Th26;
end;
theorem
dom F = dom G & (for x st x in dom F holds F.x c= G.x) implies
Product F c= Product G by Th27,CARD_1:11;
theorem
F c= G implies Sum F c= Sum G
proof
assume F c= G;
then disjoin F c= disjoin G by Th23;
hence thesis by Th24,CARD_1:11;
end;
theorem
F c= G & not 0 in rng G implies Product F c= Product G
proof
assume
A1: F c= G;
then
A2: dom F c= dom G by GRFUNC_1:2;
assume
A3: not 0 in rng G;
deffunc f(Function) = $1|dom F;
consider f such that
A4: dom f = product G & for g st g in product G holds f.g = f(g)
from FUNCT_5:sch 1;
product F c= rng f
proof
let x be object;
assume x in product F;
then consider g such that
A5: x = g and
A6: dom g = dom F and
A7: for x being object st x in dom F holds g.x in F.x by Def5;
A8: product G <> {} by A3,Th26;
set y = the Element of product G;
consider h such that
y = h
and dom h = dom G and
A9: for x being object st x in dom G holds h.x in G.x by A8,Def5;
deffunc f(object) = g.$1;
deffunc g(object) = h.$1;
defpred C[object] means $1 in dom F;
consider f1 such that
A10: dom f1 = dom G & for x being object st x in dom G holds
(C[x] implies f1.x = f(x)) & (not C[x] implies f1.x = g(x))
from PARTFUN1:sch 1;
now
let z be object such that
A11: z in dom G;
A12: now
assume
A13: z in dom F;
then
A14: f1.z = g.z by A10,A11;
g.z in F.z by A7,A13;
hence f1.z in G.z by A1,A13,A14,GRFUNC_1:2;
end;
not z in dom F implies f1.z = h.z by A10,A11;
hence f1.z in G.z by A9,A11,A12;
end;
then
A15: f1 in product G by A10,Def5;
then
A16: f.f1 = f1|dom F by A4;
A17: dom(f1|dom F) = dom F by A2,A10,RELAT_1:62;
now
let z be object;
assume
A18: z in dom F;
then (f1|dom F).z = f1.z by A17,FUNCT_1:47;
hence (f1|dom F).z = g.z by A2,A10,A18;
end;
then f.f1 = g by A6,A16,A17,FUNCT_1:2;
hence thesis by A4,A5,A15,FUNCT_1:def 3;
end;
hence thesis by A4,CARD_1:12;
end;
theorem
Sum({} --> K) = 0
proof dom ({} --> K) = {};
then dom disjoin ({} --> K) = {} by Def3;
hence thesis by CARD_1:27,RELAT_1:42,ZFMISC_1:2;
end;
theorem
Product ({} --> K) = 1 by Th10,CARD_1:30;
theorem
Sum(x .--> K) = K
proof
thus Sum(x .--> K) = card Union (x .--> [:K,{x}:]) by Th4
.= card [:K,{x}:] by Th7
.= card K by CARD_1:69
.= K;
end;
theorem
Product(x .--> K) = K
proof
thus Product(x .--> K) = card Funcs({x},K) by Th11
.= card K by FUNCT_5:58
.= K;
end;
theorem Th39:
card Union f c= Sum Card f
proof
A1: now
assume dom f = {};
then {} = Union f by RELAT_1:42,ZFMISC_1:2;
hence thesis;
end;
now
assume
A2: dom f <> {};
defpred P[set,object] means
ex A being set st A = $2 &
for x being object holds
x in A iff x in Funcs(card $1,$1) & ex g st x = g & rng g = $1;
defpred W[object,object] means P[f.$1,$2];
A3: for x being object st x in dom f ex y being object st W[x,y]
proof
let x be object such that x in dom f;
defpred A[object] means ex g st $1 = g & rng g = f.x;
consider Y such that
A4: for z being object holds z in Y iff z in Funcs(card (f.x),f.x) & A[z]
from XBOOLE_0:sch 1;
take Y;
P[f.x,Y] by A4;
hence W[x,Y];
end;
consider k being Function such that
A5: dom k = dom f &
for x being object st x in dom f holds W[x,k.x] from CLASSES1:sch 1
(A3);
reconsider M = rng k as non empty set by A2,A5,RELAT_1:42;
now
let X;
assume X in M;
then consider x being object such that
A6: x in dom k and
A7: X = k.x by FUNCT_1:def 3;
card(f.x),f.x are_equipotent by CARD_1:def 2;
then consider g such that
g is one-to-one and
A8: dom g = card(f.x) and
A9: rng g = f.x;
A10: g in Funcs(card(f.x),f.x) by A8,A9,FUNCT_2:def 2;
W[x,k.x] by A5,A6;
hence X <> {} by A7,A9,A10;
end;
then consider FF being Function such that
dom FF = M and
A11: for X st X in M holds FF.X in X by FUNCT_1:111;
set DD = union rng disjoin Card f;
defpred S[object,object] means
ex g st g = FF.(k.$1`2) & $2 = g.$1`1;
A12: for x being object st x in DD ex y being object st S[x,y]
proof
let x be object;
assume x in DD;
then consider X such that
A13: x in X and
A14: X in rng disjoin Card f by TARSKI:def 4;
consider y being object such that
A15: y in dom disjoin Card f and
A16: X = (disjoin Card f).y by A14,FUNCT_1:def 3;
A17: dom disjoin Card f = dom Card f by Def3;
A18: dom Card f = dom f by Def2;
X = [:(Card f).y,{y}:] by A15,A16,A17,Def3;
then x`2 in {y} by A13,MCART_1:10;
then
A19: x`2 in dom f by A15,A17,A18,TARSKI:def 1;
then k.x`2 in M by A5,FUNCT_1:def 3;
then
A20: FF.(k.x`2) in k.x`2 by A11;
W[x`2,k.x`2] by A5,A19;
then FF.(k.x`2) in Funcs(card (f.x`2),f.x`2) by A20;
then consider g such that
A21: FF.(k.x`2) = g
and dom g = card (f.x`2)
and rng g c= f.x`2 by FUNCT_2:def 2;
take g.x`1, g;
thus thesis by A21;
end;
consider t being Function such that
A22: dom t = DD &
for x being object st x in DD holds S[x,t.x] from CLASSES1:sch 1
(A12);
union rng f c= rng t
proof
let x be object;
assume x in union rng f;
then consider X such that
A23: x in X and
A24: X in rng f by TARSKI:def 4;
consider y being object such that
A25: y in dom f and
A26: X = f.y by A24,FUNCT_1:def 3;
k.y in M by A5,A25,FUNCT_1:def 3;
then
A27: FF.(k.y) in k.y by A11;
A28: W[y,k.y] by A5,A25;
then FF.(k.y) in Funcs(card(f.y),f.y) by A27;
then consider g such that
A29: FF.(k.y) = g and
A30: dom g = card(f.y)
and rng g c= f.y by FUNCT_2:def 2;
ex g st FF.(k.y) = g & rng g = f.y by A27,A28;
then consider z being object such that
A31: z in dom g and
A32: x = g.z by A23,A26,A29,FUNCT_1:def 3;
A33: (Card f).y = card(f.y) by A25,Def2;
A34: dom Card f = dom f by Def2;
then
A35: (disjoin Card f).y = [:dom g,{y}:] by A25,A30,A33,Def3;
A36: y in {y} by TARSKI:def 1;
A37: dom disjoin Card f = dom f by A34,Def3;
A38: [z,y] in [:dom g,{y}:] by A31,A36,ZFMISC_1:87;
[:dom g,{y}:] in rng disjoin Card f by A25,A35,A37,FUNCT_1:def 3;
then
A39: [z,y] in DD by A38,TARSKI:def 4;
A40: [z,y]`1 = z;
[z,y]`2 = y;
then ex g st g = FF.(k.y) & t.[z,y] = g.z by A22,A39,A40;
hence thesis by A22,A29,A32,A39,FUNCT_1:def 3;
end;
hence thesis by A22,CARD_1:12;
end;
hence thesis by A1;
end;
theorem
card Union F c= Sum F
proof Card F = F by Th1;
hence thesis by Th39;
end;
::$N Koenig Theorem
theorem
dom F = dom G & (for x st x in dom F holds F.x in G.x) implies
Sum F in Product G
proof
assume that
A1: dom F = dom G and
A2: for x st x in dom F holds F.x in G.x;
deffunc f(object) = (G.$1)\(F.$1);
consider f such that
A3: dom f = dom F & for x being object st x in dom F holds f.x = f(x)
from FUNCT_1:sch 3;
now
assume {} in rng f;
then consider x being object such that
A4: x in dom f and
A5: {} = f.x by FUNCT_1:def 3;
reconsider Fx = F.x, Gx = G.x as Cardinal by A1,A3,A4,Def1;
A6: Fx in Gx by A2,A3,A4;
not Fx in Fx;
then Fx in Gx \ Fx by A6,XBOOLE_0:def 5;
hence contradiction by A3,A4,A5;
end;
then
A7: product f <> {} by Th26;
set a = the Element of product f;
consider h being Function such that
a = h
and dom h = dom f and
A8: for x being object st x in dom f holds h.x in f.x by A7,Def5;
defpred P[object,Function] means dom $2 = dom F & for x st x in dom F holds
($1`2 = x implies $2.x = $1`1) & ($1`2 <> x implies $2.x = h.x);
defpred R[object,object] means ex g st $2 = g & P[$1,g];
A9: for x being object st x in Union disjoin F ex y being object st R[x,y]
proof
let x be object such that x in Union disjoin F;
deffunc f(object) = x`1;
deffunc g(object) = h.$1;
defpred C[object] means $1 = x`2;
consider g such that
A10: dom g = dom F & for u being object st u in dom F holds
(C[u] implies g.u = f(u)) & (not C[u] implies g.u = g(u))
from PARTFUN1:sch 1;
reconsider y = g as object;
take y,g;
thus thesis by A10;
end;
consider f1 such that
A11: dom f1 = Union disjoin F &
for x being object st x in Union disjoin F holds R[x,f1.x]
from CLASSES1:sch 1(A9);
A12: f1 is one-to-one
proof
let x,y be object;
assume that
A13: x in dom f1 and
A14: y in dom f1 and
A15: f1.x = f1.y and
A16: x <> y;
consider g1 being Function such that
A17: f1.x = g1 and
A18: P[x,g1] by A11,A13;
consider g2 being Function such that
A19: f1.y = g2 and
A20: P[y,g2] by A11,A14;
A21: x`2 in dom F by A11,A13,Th22;
A22: y`2 in dom F by A11,A14,Th22;
A23: y`1 in F.(y`2) by A11,A14,Th22;
A24: ex x1,x2 being object st x = [x1,x2] by A11,A13,Th21;
A25: ex x1,x2 being object st y = [x1,x2] by A11,A14,Th21;
A26: x = [x`1,x`2] by A24;
A27: y = [y`1,y`2] by A25;
A28: now
assume
A29: x`1 = y`1;
A30: g2.(y`2) = y`1 by A20,A22;
A31: g1.(y`2) = h.(y`2) by A16,A18,A22,A26,A27,A29;
A32: f.(y`2) = (G.(y`2))\(F.(y`2)) by A3,A22;
h.(y`2) in f.(y`2) by A3,A8,A22;
hence contradiction by A15,A17,A19,A23,A30,A31,A32,XBOOLE_0:def 5;
end;
A33: x`2 = y`2 implies g1.(x`2) = x`1 & g2.(x`2) = y`1 by A18,A20,A21;
A34: g1.(y`2) = y`1 by A15,A17,A19,A20,A22;
A35: g1.(y`2) = h.(y`2) by A15,A17,A18,A19,A22,A28,A33;
A36: f.(y`2) = (G.(y`2))\(F.(y`2) ) by A3,A22;
h.(y`2) in f.(y`2) by A3,A8,A22;
hence contradiction by A23,A34,A35,A36,XBOOLE_0:def 5;
end;
rng f1 c= product G
proof
let x be object;
assume x in rng f1;
then consider y being object such that
A37: y in dom f1 and
A38: x = f1.y by FUNCT_1:def 3;
consider g such that
A39: f1.y = g and
A40: P[y,g] by A11,A37;
now
let x be object;
assume
A41: x in dom G;
then reconsider Gx = G.x, Fx = F.x as Cardinal by A1,Def1;
A42: Fx in Gx by A1,A2,A41;
A43: y`2 = x implies g.x = y`1 by A1,A40,A41;
A44: y`2 <> x implies g.x = h.x by A1,A40,A41;
A45: h.x in f.x by A1,A3,A8,A41;
A46: f.x = Gx \ Fx by A1,A3,A41;
A47: y`1 in F.(y`2) by A11,A37,Th22;
Fx c= Gx by A42,CARD_1:3;
hence g.x in G.x by A43,A44,A45,A46,A47;
end;
hence thesis by A1,A38,A39,A40,Def5;
end;
then
A48: Sum F c= Product G by A11,A12,CARD_1:10;
now
assume Sum F = Product G;
then Union disjoin F,product G are_equipotent by CARD_1:5;
then consider f such that
f is one-to-one and
A49: dom f = Union disjoin F and
A50: rng f = product G;
deffunc f(object) = G.$1 \ pi(f.:((disjoin F).$1),$1);
consider K being Function such that
A51: dom K = dom F & for x being object st x in dom F holds K.x = f(x)
from FUNCT_1:sch 3;
now
assume {} in rng K;
then consider x being object such that
A52: x in dom F and
A53: {} = K.x by A51,FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
A54: K.x = G.x \ pi(f.:((disjoin F).x),x) by A51,A52;
reconsider Fx = F.x, Gx = G.x as Cardinal by A1,A52,Def1;
A55: card pi(f.:((disjoin F).x),x) c= card (f.:((disjoin F).x)) by Th20;
A56: card (f.:((disjoin F).x)) c= card ((disjoin F).x) by CARD_1:67;
card ((disjoin F).x) = Fx by A52,Th29;
then
A57: card pi(f.:((disjoin F).x),x) c= Fx by A55,A56;
A58: Fx in Gx by A2,A52;
card Gx = Gx;
hence contradiction by A53,A54,A57,A58,CARD_1:68,ORDINAL1:12;
end;
then
A59: product K <> {} by Th26;
set t = the Element of product K;
consider g such that
A60: t = g
and dom g = dom K and
A61: for x being object st x in dom K holds g.x in K.x by A59,Def5;
now
let x;
assume x in dom K;
then K.x = G.x \ pi(f.:((disjoin F).x),x) by A51;
hence K.x c= G.x;
end;
then product K c= product G by A1,A51,Th27;
then t in product G by A59;
then consider y being object such that
A62: y in dom f and
A63: t = f.y by A50,FUNCT_1:def 3;
consider X such that
A64: y in X and
A65: X in rng disjoin F by A49,A62,TARSKI:def 4;
consider x being object such that
A66: x in dom disjoin F and
A67: X = (disjoin F).x by A65,FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
g in f.:X by A60,A62,A63,A64,FUNCT_1:def 6;
then
A68: g.x in pi(f.:((disjoin F).x),x) by A67,Def6;
A69: x in dom F by A66,Def3;
A70: not g.x in G.x \ pi(f.:((disjoin F).x),x) by A68,XBOOLE_0:def 5;
g.x in (K.x) by A51,A61,A69;
hence contradiction by A51,A69,A70;
end;
hence thesis by A48,CARD_1:3;
end;
scheme FuncSeparation { X()->set, F(object)->set, P[object,object] }:
ex f st dom f = X() &
for x being object st x in X()
for y being object holds y in f.x iff y in F(x) & P[x,y]
proof
defpred Q[object,object] means
ex A being set st A = $2 &
for y holds y in A iff y in F($1) & P[$1,y];
A1: for x being object st x in X() ex y being object st Q[x,y]
proof
let x be object such that x in X();
defpred R[object] means P[x,$1];
consider Y such that
A2: for y being object holds y in Y iff y in F(x) & R[y] from XBOOLE_0:sch 1;
take Y;
reconsider A = Y as set;
take A;
thus A = Y &
for y holds y in A iff y in F(x) & P[x,y] by A2;
end;
consider f such that
A3: dom f = X() and
A4: for x being object st x in X() holds Q[x,f.x] from CLASSES1:sch 1(A1);
take f;
thus dom f = X() by A3;
let x be object;
assume x in X();
then consider A being set such that
A5: A = f.x and
A6: for y holds y in A iff y in F(x) & P[x,y] by A4;
thus thesis by A5,A6;
end;
Lm1: x in field R implies ex y being object st [x,y] in R or [y,x] in R
proof
assume x in field R;
then x in dom R or x in rng R by XBOOLE_0:def 3;
hence thesis by XTUPLE_0:def 12,def 13;
end;
theorem Th42:
X is finite implies card X in card omega
proof
assume X is finite;
then ex n being Nat st ( card X = card n) by CARD_1:48;
hence thesis;
end;
theorem Th43:
card A in card B implies A in B
proof
assume that
A1: card A in card B and
A2: not A in B;
not card B c= card A by A1,CARD_1:4;
hence contradiction by A2,CARD_1:11,ORDINAL1:16;
end;
theorem Th44:
card A in M implies A in M
proof
card M = M;
hence thesis by Th43;
end;
theorem Th45:
X is c=-linear implies
ex Y st Y c= X & union Y = union X & for Z st Z c= Y & Z <> {}
ex Z1 st Z1 in Z & for Z2 st Z2 in Z holds Z1 c= Z2
proof
assume
A1: X is c=-linear;
consider R such that
A2: R well_orders X by WELLORD2:17;
A3: R|_2 X is well-ordering by A2,WELLORD2:16;
A4: field(R|_2 X) = X by A2,WELLORD2:16;
R|_2 X, RelIncl order_type_of R|_2 X are_isomorphic by A3,WELLORD2:def 2;
then RelIncl order_type_of R|_2 X, R|_2 X are_isomorphic by WELLORD1:40;
then consider f such that
A5: f is_isomorphism_of RelIncl order_type_of R|_2 X, R|_2 X;
field RelIncl order_type_of R|_2 X = order_type_of R|_2 X by WELLORD2:def 1;
then
A6: dom f = order_type_of R|_2 X by A5;
A7: rng f = X by A4,A5;
defpred P[object] means for A,B st B in A & $1 = A holds f.B c= f.A;
consider Y such that
A8: for x being set holds x in Y iff x in dom f & P[x] from XFAMILY:sch 1;
take Z = f.:Y;
thus Z c= X by A7,RELAT_1:111;
thus union Z c= union X by A7,RELAT_1:111,ZFMISC_1:77;
thus union X c= union Z
proof
let x be object;
assume x in union X;
then consider Z1 such that
A9: x in Z1 and
A10: Z1 in X by TARSKI:def 4;
consider y being object such that
A11: y in dom f and
A12: Z1 = f.y by A7,A10,FUNCT_1:def 3;
reconsider y as Ordinal by A6,A11;
defpred P[Ordinal] means $1 c= y & x in f.$1;
A13: ex A st P[A] by A9,A12;
consider A such that
A14: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A13);
A15: A in dom f by A6,A11,A14,ORDINAL1:12;
now
let B,C;
assume that
A16: C in B and
A17: A = B;
A18: C in dom f by A6,A11,A14,A16,A17,ORDINAL1:10;
A19: not C c= y or not x in f.C by A14,A16,A17,ORDINAL1:5;
A20: f.A in X by A7,A15,FUNCT_1:def 3;
f.C in X by A7,A18,FUNCT_1:def 3;
then f.C,f.A are_c=-comparable by A1,A20;
then f.C c= f.A or f.A c= f.C;
hence f.C c= f.B by A14,A16,A17,A19,ORDINAL1:def 2;
end;
then A in Y by A8,A15;
then f.A in Z by A15,FUNCT_1:def 6;
hence thesis by A14,TARSKI:def 4;
end;
let V be set;
assume that
A21: V c= Z and
A22: V <> {};
set x = the Element of V;
x in Z by A21,A22;
then consider y being object such that
A23: y in dom f and
A24: y in Y and
A25: x = f.y by FUNCT_1:def 6;
reconsider y as Ordinal by A6,A23;
defpred P[Ordinal] means $1 in Y & f.$1 in V;
y = y;
then
A26: ex A st P[A] by A22,A24,A25;
consider A such that
A27: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A26);
take Z1 = f.A;
thus Z1 in V by A27;
let Z2;
assume
A28: Z2 in V;
then consider y being object such that
A29: y in dom f and
A30: y in Y and
A31: Z2 = f.y by A21,FUNCT_1:def 6;
reconsider y as Ordinal by A6,A29;
A c< y iff A c= y & A <> y;
then A = y or A in y by A27,A28,A30,A31,ORDINAL1:11;
hence thesis by A8,A30,A31;
end;
theorem
(for Z st Z in X holds card Z in M) & X is c=-linear implies
card union X c= M
proof
assume that
A1: Z in X implies card Z in M and
A2: X is c=-linear;
consider XX being set such that
A3: XX c= X and
A4: union XX = union X and
A5: for Z st Z c= XX & Z <> {}
ex Z1 st Z1 in Z & for Z2 st Z2 in Z holds Z1 c= Z2 by A2,Th45;
A6: for Z1,Z2 st Z1 in XX & Z2 in XX holds Z1 c= Z2 or Z2 c= Z1
by A2,A3,XBOOLE_0:def 9;
consider R such that
A7: R well_orders union X by WELLORD2:17;
A8: R is_reflexive_in union X by A7;
A9: R is_transitive_in union X by A7;
A10: R is_antisymmetric_in union X by A7;
A11: R is_connected_in union X by A7;
defpred P[object,object] means
((ex Z1 st Z1 in XX & $1 in Z1 & not $2 in Z1) or
(for Z1 st Z1 in XX holds $1 in Z1 iff $2 in Z1) & [$1,$2] in R);
consider Q such that
A12: for x,y being object holds
[x,y] in Q iff x in union X & y in union X & P[x,y] from RELAT_1:sch 1;
A13: field Q = union X
proof
thus field Q c= union X
proof
let x be object;
assume x in field Q;
then ex y being object st [x,y] in Q or [y,x] in Q by Lm1;
hence thesis by A12;
end;
let x be object;
assume
A14: x in union X;
then
A15: [x,x] in R by A8;
for Z1 st Z1 in XX holds x in Z1 iff x in Z1;
then [x,x] in Q by A12,A14,A15;
hence thesis by RELAT_1:15;
end;
A16: Q is reflexive
proof
let x be object;
assume
A17: x in field Q;
then
A18: [x,x] in R by A8,A13;
for Z1 st Z1 in XX holds x in Z1 iff x in Z1;
hence thesis by A12,A13,A17,A18;
end;
A19: Q is transitive
proof
let x,y,z be object such that
A20: x in field Q and
A21: y in field Q and
A22: z in field Q and
A23: [x,y] in Q and
A24: [y,z] in Q;
A25: now
given Z1 such that
A26: Z1 in XX and
A27: x in Z1 and
A28: not y in Z1;
given Z2 such that
A29: Z2 in XX and
A30: y in Z2 and
A31: not z in Z2;
Z1 c= Z2 or Z2 c= Z1 by A6,A26,A29;
hence thesis by A12,A13,A20,A22,A27,A28,A29,A30,A31;
end;
A32: now
given Z1 such that
A33: Z1 in XX and
A34: x in Z1 and
A35: not y in Z1;
assume that
A36: for Z1 st Z1 in XX holds y in Z1 iff z in Z1
and [y,z] in R;
not z in Z1 by A33,A35,A36;
hence thesis by A12,A13,A20,A22,A33,A34;
end;
A37: now
given Z1 such that
A38: Z1 in XX and
A39: y in Z1 and
A40: not z in Z1;
assume that
A41: for Z1 st Z1 in XX holds x in Z1 iff y in Z1
and [x,y] in R;
x in Z1 by A38,A39,A41;
hence thesis by A12,A13,A20,A22,A38,A40;
end;
now
assume that
A42: for Z1 st Z1 in XX holds x in Z1 iff y in Z1 and
A43: [x,y] in R and
A44: for Z1 st Z1 in XX holds y in Z1 iff z in Z1 and
A45: [y,z] in R;
A46: [x,z] in R by A9,A13,A20,A21,A22,A43,A45;
now
let Z;
assume
A47: Z in XX;
then x in Z iff y in Z by A42;
hence x in Z iff z in Z by A44,A47;
end;
hence thesis by A12,A13,A20,A22,A46;
end;
hence thesis by A12,A23,A24,A25,A32,A37;
end;
A48: Q is antisymmetric
proof
let x,y be object;
assume that
A49: x in field Q and
A50: y in field Q and
A51: [x,y] in Q and
A52: [y,x] in Q;
A53: (ex Z1 st Z1 in XX & x in Z1 & not y in Z1) or (for Z1 st Z1 in XX
holds x in Z1 iff y in Z1) & [x,y] in R by A12,A51;
A54: (ex Z1 st Z1 in XX & y in Z1 & not x in Z1) or (for Z1 st Z1 in XX
holds y in Z1 iff x in Z1) & [y,x] in R by A12,A52;
now
given Z1 such that
A55: Z1 in XX and
A56: x in Z1 and
A57: not y in Z1;
given Z2 such that
A58: Z2 in XX and
A59: y in Z2 and
A60: not x in Z2;
Z1 c= Z2 or Z2 c= Z1 by A6,A55,A58;
hence thesis by A56,A57,A59,A60;
end;
hence thesis by A10,A13,A49,A50,A53,A54;
end;
A61: Q is connected
proof
let x,y be object such that
A62: x in field Q and
A63: y in field Q and
A64: x <> y;
now
assume
A65: for Z st Z in XX holds x in Z iff y in Z;
A66: [x,y] in R or [y,x] in R by A11,A13,A62,A63,A64;
for Z st Z in XX holds y in Z iff x in Z by A65;
hence thesis by A12,A13,A62,A63,A65,A66;
end;
hence thesis by A12,A13,A62,A63;
end;
Q is well_founded
proof
let Y such that
A67: Y c= field Q and
A68: Y <> {};
defpred P[set] means $1 /\ Y <> {};
consider Z such that
A69: for x being set holds x in Z iff x in XX & P[x] from XFAMILY:sch 1;
A70: Z c= XX
by A69;
set x = the Element of Y;
x in union XX by A4,A13,A67,A68;
then consider Z1 such that
A71: x in Z1 and
A72: Z1 in XX by TARSKI:def 4;
Z1 /\ Y <> {} by A68,A71,XBOOLE_0:def 4;
then Z <> {} by A69,A72;
then consider Z1 such that
A73: Z1 in Z and
A74: for Z2 st Z2 in Z holds Z1 c= Z2 by A5,A70;
A75: Z1 in XX by A69,A73;
A76: Z1 /\ Y c= Z1 by XBOOLE_1:17;
A77: Z1 c= union X by A3,A75,ZFMISC_1:74;
Z1 /\ Y <> {} by A69,A73;
then consider x being object such that
A78: x in Z1 /\ Y and
A79: for y being object st y in Z1 /\ Y holds [x,y] in R
by A7,A76,A77,WELLORD1:5,XBOOLE_1:1;
take x;
thus x in Y by A78,XBOOLE_0:def 4;
assume
A80: Q-Seg x /\ Y <> {};
set y = the Element of Q-Seg x /\ Y;
A81: x in Z1 by A78,XBOOLE_0:def 4;
A82: y in Q-Seg x by A80,XBOOLE_0:def 4;
A83: y in Y by A80,XBOOLE_0:def 4;
A84: y <> x by A82,WELLORD1:1;
A85: [y,x] in Q by A82,WELLORD1:1;
A86: now
given Z2 such that
A87: Z2 in XX and
A88: y in Z2 and
A89: not x in Z2;
Z2 /\ Y <> {} by A83,A88,XBOOLE_0:def 4;
then Z2 in Z by A69,A87;
then Z1 c= Z2 by A74;
hence contradiction by A81,A89;
end;
then
A90: y in Z1 by A12,A75,A81,A85;
A91: [y,x] in R by A12,A85,A86;
y in Z1 /\ Y by A83,A90,XBOOLE_0:def 4;
then
A92: [x,y] in R by A79;
A93: x in union X by A12,A85;
y in union X by A12,A85;
hence contradiction by A10,A84,A91,A92,A93;
end;
then Q is well-ordering by A16,A19,A48,A61;
then Q,RelIncl order_type_of Q are_isomorphic by WELLORD2:def 2;
then RelIncl order_type_of Q,Q are_isomorphic by WELLORD1:40;
then consider g such that
A94: g is_isomorphism_of RelIncl order_type_of Q,Q;
A95: field RelIncl order_type_of Q = order_type_of Q by WELLORD2:def 1;
then
A96: dom g = order_type_of Q by A94;
A97: rng g = union X by A13,A94;
A98: g is one-to-one by A94;
A99: for Z,x st Z in XX & x in Z holds Q-Seg x c= Z
proof
let Z,x such that
A100: Z in XX and
A101: x in Z;
let y be object;
assume y in Q-Seg x;
then
A102: [y,x] in Q by WELLORD1:1;
now
given Z1 such that
A103: Z1 in XX and
A104: y in Z1 and
A105: not x in Z1;
Z1 c= Z or Z c= Z1 by A6,A100,A103;
hence thesis by A101,A104,A105;
end;
hence thesis by A12,A100,A101,A102;
end;
A106: for A st A in order_type_of Q holds card A = card (Q-Seg(g.A))
proof
let A such that
A107: A in order_type_of Q;
A,Q-Seg(g.A) are_equipotent
proof
take f = g|A;
A c= dom g by A96,A107,ORDINAL1:def 2;
hence
A108: f is one-to-one & dom f = A by A98,FUNCT_1:52,RELAT_1:62;
thus rng f c= Q-Seg(g.A)
proof
let x be object;
assume x in rng f;
then consider y being object such that
A109: y in dom f and
A110: x = f.y by FUNCT_1:def 3;
reconsider B = y as Ordinal by A108,A109;
A111: B in order_type_of Q by A107,A108,A109,ORDINAL1:10;
B c= A by A108,A109,ORDINAL1:def 2;
then
A112: [B,A] in RelIncl order_type_of Q by A107,A111,WELLORD2:def 1;
A113: x = g.B by A109,A110,FUNCT_1:47;
reconsider BB = B as set;
not BB in BB; then
A114: A <> B by A108,A109;
A115: [x,g.A] in Q by A94,A112,A113;
x <> g.A by A96,A98,A107,A111,A113,A114;
hence thesis by A115,WELLORD1:1;
end;
let x be object;
assume
A116: x in Q-Seg(g.A);
then
A117: [x,g.A] in Q by WELLORD1:1;
then x in union X by A12;
then consider y being object such that
A118: y in dom g and
A119: x = g.y by A97,FUNCT_1:def 3;
reconsider B = y as Ordinal by A96,A118;
[B,A] in RelIncl order_type_of Q by A94,A95,A107,A117,A118,A119;
then
A120: B c= A by A96,A107,A118,WELLORD2:def 1;
B <> A by A116,A119,WELLORD1:1;
then B c< A by A120;
hence thesis by A118,A119,FUNCT_1:50,ORDINAL1:11;
end;
hence thesis by CARD_1:5;
end;
A121: order_type_of Q c= M
proof
let x be Ordinal;
assume
A122: x in order_type_of Q;
reconsider A = x as Ordinal;
g.x in union X by A96,A97,A122,FUNCT_1:def 3;
then consider Z such that
A123: g.x in Z and
A124: Z in XX by A4,TARSKI:def 4;
A125: card (Q-Seg(g.x)) c= card Z by A99,A123,A124,CARD_1:11;
A126: card (Q-Seg(g.x)) = card A by A106,A122;
card (Q-Seg(g.x)) in M by A1,A3,A124,A125,ORDINAL1:12;
hence thesis by A126,Th44;
end;
order_type_of Q,union X are_equipotent by A96,A97,A98;
then
A127: card order_type_of Q = card union X by CARD_1:5;
card M = M;
hence thesis by A121,A127,CARD_1:11;
end;
begin :: Addenda
:: from AMI_1
registration
let f be Function;
cluster product f -> functional;
coherence
proof
set d = product f;
let x be object;
assume x in d;
then ex g being Function
st x = g & dom g= dom f &
for x being object st x in dom f holds g.x in f.x by Def5;
hence thesis;
end;
end;
registration
let A be set;
let B be with_non-empty_elements set;
cluster -> non-empty for Function of A,B;
coherence
proof
let f be Function of A,B;
thus not {} in rng f;
end;
end;
:: from PRVECT_1
registration
let f be non-empty Function;
cluster product f -> non empty;
coherence
proof
not {} in rng f;
hence thesis by Th26;
end;
end;
:: from AMI_1, 2006.03.14, A.T.
theorem
for a,b,c,d being set st a <> b holds
product (a,b) --> ({c},{d}) = { (a,b) --> (c,d) }
proof
let a,b,c,d be set such that
A1: a <> b;
set X = { (a,b) --> (c,d) }, f = (a,b) --> ({c},{d});
A2: dom f = {a,b} by FUNCT_4:62;
now
let x be object;
thus x in X implies ex g being Function st x = g & dom g = dom f &
for x being object st x in dom f holds g.x in f.x
proof
assume
A3: x in X;
take g = (a,b) --> (c,d);
thus x = g by A3,TARSKI:def 1;
thus dom g = dom f by A2,FUNCT_4:62;
let x be object;
assume x in dom f;
then
A4: x = a or x = b by A2,TARSKI:def 2;
A5: g.a = c by A1,FUNCT_4:63;
A6: f.a = {c} by A1,FUNCT_4:63;
A7: g.b = d by FUNCT_4:63;
f.b = {d} by FUNCT_4:63;
hence thesis by A4,A5,A6,A7,TARSKI:def 1;
end;
given g being Function such that
A8: x = g and
A9: dom g = dom f and
A10: for x being object st x in dom f holds g.x in f.x;
A11: a in dom f by A2,TARSKI:def 2;
A12: b in dom f by A2,TARSKI:def 2;
A13: g.a in f.a by A10,A11;
A14: g.b in f.b by A10,A12;
A15: f.a = {c} by A1,FUNCT_4:63;
A16: f.b = {d} by FUNCT_4:63;
A17: g.a = c by A13,A15,TARSKI:def 1;
g.b = d by A14,A16,TARSKI:def 1;
then g = (a,b) --> (c,d) by A2,A9,A17,FUNCT_4:66;
hence x in X by A8,TARSKI:def 1;
end;
hence thesis by Def5;
end;
:: from AMI_1, 2006.03.14, A.T.
theorem
x in product f implies x is Function;
begin :: Superproducts, from AMI_1, 2006.03.14, A.T.
reserve A,B for set;
definition
let f be Function;
func sproduct f -> set means
:Def9:
for x being object holds x in it iff ex g st x = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x;
existence
proof
defpred P[object] means ex g st $1 = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x;
consider A being set such that
A1: for x being object holds
x in A iff x in PFuncs(dom f, union rng f) & P[x] from XBOOLE_0:sch 1;
now
let x be object;
thus x in A implies ex g st x = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x by A1;
given g such that
A2: x = g and
A3: dom g c= dom f and
A4: for x being object st x in dom g holds g.x in f.x;
rng g c= union rng f
proof
let y be object;
assume y in rng g;
then consider z being object such that
A5: z in dom g and
A6: y = g.z by FUNCT_1:def 3;
A7: g.z in f.z by A4,A5;
f.z in rng f by A3,A5,FUNCT_1:def 3;
hence thesis by A6,A7,TARSKI:def 4;
end;
then x in PFuncs(dom f, union rng f) by A2,A3,PARTFUN1:def 3;
hence x in A by A1,A2,A3,A4;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means ex g st $1 = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x;
let A,B be set such that
A8: for x being object holds x in A iff P[x] and
A9: for x being object holds x in B iff P[x];
thus thesis from XBOOLE_0:sch 2(A8,A9);
end;
end;
registration
let f be Function;
cluster sproduct f -> functional non empty;
coherence
proof
defpred P[object] means ex g st $1 = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x;
consider A being set such that
A1: for x being object holds
x in A iff x in PFuncs(dom f, union rng f) & P[x]
from XBOOLE_0:sch 1;
{} is PartFunc of dom f, union rng f by RELSET_1:12;
then
A2: {} in PFuncs(dom f, union rng f) by PARTFUN1:45;
A3: dom {} c= dom f;
A4: for x being object st x in dom {} holds {} .x in f.x;
now
let x be object;
assume x in A;
then ex g st x = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x by A1;
hence x is Function;
end;
then reconsider A as functional non empty set by A1,A2,A3,A4,FUNCT_1:def 13
;
now
let x be object;
thus x in A implies ex g st x = g & dom g c= dom f &
for x being object st x in dom g holds g.x in f.x by A1;
given g such that
A5: x = g and
A6: dom g c= dom f and
A7: for x being object st x in dom g holds g.x in f.x;
rng g c= union rng f
proof
let y be object;
assume y in rng g;
then consider z being object such that
A8: z in dom g and
A9: y = g.z by FUNCT_1:def 3;
A10: g.z in f.z by A7,A8;
f.z in rng f by A6,A8,FUNCT_1:def 3;
hence thesis by A9,A10,TARSKI:def 4;
end;
then x in PFuncs(dom f, union rng f) by A5,A6,PARTFUN1:def 3;
hence x in A by A1,A5,A6,A7;
end;
hence thesis by Def9;
end;
end;
theorem Th49:
g in sproduct f implies dom g c= dom f &
for x st x in dom g holds g.x in f.x
proof
assume g in sproduct f;
then ex h st g = h & dom h c= dom f &
for x being object st x in dom h holds h.x in f.x by Def9;
hence thesis;
end;
theorem Th50:
{} in sproduct f
proof
A1: dom {} c= dom f;
for x being object st x in dom {} holds {} .x in f.x;
hence thesis by A1,Def9;
end;
registration let f;
cluster empty for Element of sproduct f;
existence
proof
{} in sproduct f by Th50;
hence thesis;
end;
end;
theorem Th51:
product f c= sproduct f
proof
let x be object;
assume x in product f;
then ex g st x = g & dom g = dom f &
for x being object st x in dom f holds g.x in f.x by Def5;
hence thesis by Def9;
end;
theorem Th52:
x in sproduct f implies x is PartFunc of dom f, union rng f
proof
assume x in sproduct f;
then consider g such that
A1: x = g and
A2: dom g c= dom f and
A3: for x being object st x in dom g holds g.x in f.x by Def9;
rng g c= union rng f
proof
let y be object;
assume y in rng g;
then consider z being object such that
A4: z in dom g and
A5: y = g.z by FUNCT_1:def 3;
A6: g.z in f.z by A3,A4;
f.z in rng f by A2,A4,FUNCT_1:def 3;
hence thesis by A5,A6,TARSKI:def 4;
end;
hence thesis by A1,A2,RELSET_1:4;
end;
theorem Th53:
g in product f & h in sproduct f implies g +* h in product f
proof
assume
A1: g in product f;
then
A2: dom g = dom f by Th9;
assume
A3: h in sproduct f;
then
A4: dom g \/ dom h = dom f by A2,Th49,XBOOLE_1:12;
then
A5: dom(g +* h) = dom f by FUNCT_4:def 1;
now
let x be object;
assume
A6: x in dom f;
A7: (dom g \ dom h) \/ dom h = dom f by A4,XBOOLE_1:39;
now per cases by A6,A7,XBOOLE_0:def 3;
case
A8: x in dom g \ dom h;
then not x in dom h by XBOOLE_0:def 5;
hence x in dom f & (g +* h).x = g.x by A2,A8,FUNCT_4:11;
end;
case x in dom h;
hence (g +* h).x = h.x by FUNCT_4:13;
end;
end;
hence (g +* h).x in f.x by A1,A3,Th9,Th49;
end;
hence thesis by A5,Th9;
end;
theorem
product f <> {} implies
(g in sproduct f iff ex h st h in product f & g c= h)
proof
assume
A1: product f <> {};
thus g in sproduct f implies ex h st h in product f & g c= h
proof
assume
A2: g in sproduct f;
set k = the Element of product f;
reconsider k as Function;
take k +* g;
thus k +* g in product f by A1,A2,Th53;
thus thesis by FUNCT_4:25;
end;
given h such that
A3: h in product f and
A4: g c= h;
A5: dom h = dom f by A3,Th9;
A6: dom g c= dom h by A4,RELAT_1:11;
now
let x be object;
assume
A7: x in dom g;
then g.x = h.x by A4,GRFUNC_1:2;
hence g.x in f.x by A3,A5,A6,A7,Th9;
end;
hence thesis by A5,A6,Def9;
end;
theorem Th55:
sproduct f c= PFuncs(dom f,union rng f)
proof
let x be object;
assume x in sproduct f;
then x is PartFunc of dom f, union rng f by Th52;
hence thesis by PARTFUN1:45;
end;
theorem Th56:
f c= g implies sproduct f c= sproduct g
proof
assume
A1: f c= g;
then
A2: dom f c= dom g by GRFUNC_1:2;
let y be object;
assume y in sproduct f;
then consider h such that
A3: y = h and
A4: dom h c= dom f and
A5: for x being object st x in dom h holds h.x in f.x by Def9;
A6: dom h c= dom g by A2,A4;
now
let x be object;
assume
A7: x in dom h;
then f.x = g.x by A1,A4,GRFUNC_1:2;
hence h.x in g.x by A5,A7;
end;
hence thesis by A3,A6,Def9;
end;
theorem Th57:
sproduct {} = {{}}
proof
sproduct {} c= PFuncs({},{}) by Th55,RELAT_1:38,ZFMISC_1:2;
hence sproduct {} c= {{}} by PARTFUN1:48;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
hence thesis by Th50;
end;
theorem
PFuncs(A,B) = sproduct (A --> B)
proof
now per cases;
case
A = {};
then A --> B = {} --> B;
hence thesis by Th57,PARTFUN1:48;
end;
case A <> {};
then
A2: rng (A --> B) = { B } by FUNCOP_1:8;
A3: dom(A --> B) = A;
A4: B = union rng (A --> B) by A2,ZFMISC_1:25;
thus PFuncs(A,B) c= sproduct (A --> B)
proof
let x be object;
assume x in PFuncs(A,B);
then consider f being Function such that
A5: x = f and
A6: dom f c= A and
A7: rng f c= B by PARTFUN1:def 3;
A8: dom f c= dom (A --> B) by A6;
now
let x be object;
assume
A9: x in dom f;
then f.x in rng f by FUNCT_1:def 3;
then f.x in B by A7;
hence f.x in (A --> B).x by A6,A9,FUNCOP_1:7;
end;
hence thesis by A5,A8,Def9;
end;
thus sproduct (A --> B) c= PFuncs(A,B) by A3,A4,Th55;
end;
end;
hence thesis;
end;
theorem
for A, B being non empty set for f being Function of A,B
holds sproduct f = sproduct(f|{x where x is Element of A: f.x <> {} })
proof
let A, B be non empty set;
let f be Function of A,B;
set X = {x where x is Element of A: f.x <> {} };
thus sproduct f c= sproduct(f|X)
proof
let x be object;
assume x in sproduct f;
then consider g such that
A1: x = g and
A2: dom g c= dom f and
A3: for x being object st x in dom g holds g.x in f.x by Def9;
A4: now
let x;
assume
A5: x in dom g;
then reconsider a = x as Element of A by A2,FUNCT_2:def 1;
f.a <> {} by A3,A5;
hence x in X;
end;
A6: now
let x;
assume
A7: x in dom g;
then x in X by A4;
hence x in (dom f)/\ X by A2,A7,XBOOLE_0:def 4;
end;
A8: dom g c= dom(f|X)
proof
let x be object;
assume x in dom g;
then x in (dom f)/\ X by A6;
hence thesis by RELAT_1:61;
end;
now
let x be object;
assume
A9: x in dom g;
then g.x in f.x by A3;
hence g.x in (f|X).x by A6,A9,FUNCT_1:48;
end;
hence thesis by A1,A8,Def9;
end;
thus thesis by Th56,RELAT_1:59;
end;
theorem Th60:
x in dom f & y in f.x implies x .--> y in sproduct f
proof
assume that
A1: x in dom f and
A2: y in f.x;
A3: dom(x .--> y) c= dom f by A1,ZFMISC_1:31;
now
let z be object;
assume z in dom(x .--> y);
then z = x by TARSKI:def 1;
hence (x .--> y).z in f.z by A2,FUNCOP_1:72;
end;
hence thesis by A3,Def9;
end;
theorem
sproduct f = {{}} iff for x st x in dom f holds f.x = {}
proof
thus sproduct f = {{}} implies for x st x in dom f holds f.x = {}
proof
assume
A1: sproduct f = {{}};
let x;
assume
A2: x in dom f;
assume
A3: f.x <> {};
set y = the Element of f.x;
x .--> y in sproduct f by A2,A3,Th60;
hence contradiction by A1,TARSKI:def 1;
end;
assume
A4: for x st x in dom f holds f.x = {};
now
let x be object;
thus x in sproduct f implies x = {}
proof
assume x in sproduct f;
then consider g such that
A5: x = g and
A6: dom g c= dom f and
A7: for y being object st y in dom g holds g.y in f.y by Def9;
assume
A8: x <> {};
set y = the Element of dom g;
A9: f.y <> {} by A5,A7,A8;
y in dom f by A5,A6,A8;
hence contradiction by A4,A9;
end;
thus x = {} implies x in sproduct f by Th50;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th62:
A c= sproduct f &
(for h1,h2 being Function st h1 in A & h2 in A holds h1 tolerates h2)
implies union A in sproduct f
proof
assume that
A1: A c= sproduct f and
A2: for h1,h2 being Function st h1 in A & h2 in A holds h1 tolerates h2;
reconsider g = union A as Function by A1,A2,PARTFUN1:78;
A3: dom g c= dom f
proof
let x be object;
assume x in dom g;
then consider y being object such that
A4: [x,y] in g by XTUPLE_0:def 12;
consider h being set such that
A5: [x,y] in h and
A6: h in A by A4,TARSKI:def 4;
reconsider h as Function by A1,A6;
A7: x in dom h by A5,XTUPLE_0:def 12;
dom h c= dom f by A1,A6,Th49;
hence thesis by A7;
end;
now
let x be object;
assume x in dom g;
then consider y being object such that
A8: [x,y] in g by XTUPLE_0:def 12;
consider h being set such that
A9: [x,y] in h and
A10: h in A by A8,TARSKI:def 4;
reconsider h as Function by A1,A10;
A11: x in dom h by A9,XTUPLE_0:def 12;
h.x = y by A9,FUNCT_1:1
.= g.x by A8,FUNCT_1:1;
hence g.x in f.x by A1,A10,A11,Th49;
end;
hence thesis by A3,Def9;
end;
theorem
g tolerates h & g in sproduct f & h in sproduct f
implies g \/ h in sproduct f
proof
assume that
A1: g tolerates h and
A2: g in sproduct f and
A3: h in sproduct f;
A4: {g,h} c= sproduct f by A2,A3,ZFMISC_1:32;
A5: now
let h1,h2 be Function;
assume that
A6: h1 in {g,h} and
A7: h2 in {g,h};
A8: h1 = g or h1 = h by A6,TARSKI:def 2;
h2 = g or h2 = h by A7,TARSKI:def 2;
hence h1 tolerates h2 by A1,A8;
end;
union {g,h} = g \/ h by ZFMISC_1:75;
hence thesis by A4,A5,Th62;
end;
theorem Th64:
for x being set holds
x c= h & h in sproduct f implies x in sproduct f
proof let x be set;
assume that
A1: x c= h and
A2: h in sproduct f;
reconsider g = x as Function by A1;
A3: dom g c= dom h by A1,GRFUNC_1:2;
dom h c= dom f by A2,Th49;
then
A4: dom g c= dom f by A3;
now
let x be object;
assume
A5: x in dom g;
then h.x in f.x by A2,A3,Th49;
hence g.x in f.x by A1,A5,GRFUNC_1:2;
end;
hence thesis by A4,Def9;
end;
theorem Th65:
g in sproduct f implies g|A in sproduct f by Th64,RELAT_1:59;
theorem Th66:
g in sproduct f implies g|A in sproduct f|A
proof
A1: dom(g|A) = dom g /\ A by RELAT_1:61;
A2: dom(f|A) = dom f /\ A by RELAT_1:61;
assume
A3: g in sproduct f;
then
A4: dom(g|A) c= dom(f|A) by A1,A2,Th49,XBOOLE_1:26;
now
let x be object;
assume
A5: x in dom(g|A);
then
A6: (g|A).x = g.x by FUNCT_1:47;
A7: (f|A).x = f.x by A4,A5,FUNCT_1:47;
x in dom g by A1,A5,XBOOLE_0:def 4;
hence (g|A).x in (f|A).x by A3,A6,A7,Th49;
end;
hence thesis by A4,Def9;
end;
theorem
h in sproduct(f+*g) implies
ex f9,g9 being Function st f9 in sproduct f & g9 in sproduct g & h = f9+*g9
proof
assume
A1: h in sproduct(f+*g);
take h|(dom f \ dom g), h|dom g;
A2: h|(dom f \ dom g) in sproduct (f +* g)|(dom f \ dom g) by A1,Th66;
sproduct (f +* g)|(dom f \ dom g) c= sproduct f by Th56,FUNCT_4:24;
hence h|(dom f \ dom g) in sproduct f by A2;
(f +* g)|dom g = g;
hence h|dom g in sproduct g by A1,Th66;
dom h c= dom(f+*g) by A1,Th49;
then dom h c= dom f \/ dom g by FUNCT_4:def 1;
then dom h c= (dom f \ dom g) \/ dom g by XBOOLE_1:39;
hence thesis by FUNCT_4:70;
end;
theorem Th68:
for f9,g9 being Function st dom g misses dom f9 \ dom g9 &
f9 in sproduct f & g9 in sproduct g holds f9+*g9 in sproduct(f+*g)
proof
let f9,g9 be Function such that
A1: dom g misses dom f9 \ dom g9 and
A2: f9 in sproduct f and
A3: g9 in sproduct g;
set h = f9+*g9;
A4: dom f9 c= dom f by A2,Th49;
A5: dom g9 c= dom g by A3,Th49;
then
A6: dom f9 \/ dom g9 c= dom f \/ dom g by A4,XBOOLE_1:13;
A7: dom h = dom f9 \/ dom g9 by FUNCT_4:def 1;
then
A8: dom h c= dom(f+*g) by A6,FUNCT_4:def 1;
for x being object holds x in dom h implies h.x in (f+*g).x
proof let x be object;
assume
A9: x in dom h;
then x in dom(f+*g) by A8;
then
A10: x in dom f \/ dom g by FUNCT_4:def 1;
x in dom f9 \ dom g9 \/ dom g9 by A7,A9,XBOOLE_1:39;
then
A11: x in dom f9 \ dom g9 or x in dom g9 by XBOOLE_0:def 3;
now per cases;
case
A12: x in dom g;
then h.x = g9.x by A1,A7,A9,A11,FUNCT_4:def 1,XBOOLE_0:3;
hence h.x in g.x by A1,A3,A11,A12,Th49,XBOOLE_0:3;
end;
case not x in dom g;
then
A13: not x in dom g9 by A5;
then
A14: h.x = f9.x by A7,A9,FUNCT_4:def 1;
x in dom f9 by A7,A9,A13,XBOOLE_0:def 3;
hence h.x in f.x by A2,A14,Th49;
end;
end;
hence thesis by A10,FUNCT_4:def 1;
end;
hence thesis by A8,Def9;
end;
theorem
for f9,g9 being Function st dom f9 misses dom g \ dom g9 &
f9 in sproduct f & g9 in sproduct g holds f9+*g9 in sproduct(f+*g)
proof
let f9,g9 be Function;
assume dom f9 misses dom g \ dom g9;
then dom g misses dom f9 \ dom g9 by XBOOLE_1:81;
hence thesis by Th68;
end;
theorem Th70:
g in sproduct f & h in sproduct f implies g +* h in sproduct f
proof
assume that
A1: g in sproduct f and
A2: h in sproduct f;
A3: dom g c= dom f by A1,Th49;
dom h c= dom f by A2,Th49;
then dom g \/ dom h c= dom f by A3,XBOOLE_1:8;
then
A4: dom(g+*h) c= dom f by FUNCT_4:def 1;
now
let x be object;
assume x in dom(g+*h);
then x in dom g \/ dom h by FUNCT_4:def 1;
then
A5: x in (dom g \ dom h \/ dom h) by XBOOLE_1:39;
now per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in dom h;
then h.x in f.x by A2,Th49;
hence (g+*h).x in f.x by A6,FUNCT_4:13;
end;
suppose
A7: x in dom g \ dom h;
then
A8: g.x in f.x by A1,Th49;
not x in dom h by A7,XBOOLE_0:def 5;
hence (g+*h).x in f.x by A8,FUNCT_4:11;
end;
end;
hence (g+*h).x in f.x;
end;
hence thesis by A4,Def9;
end;
theorem
for x1,x2,y1,y2 being set holds
x1 in dom f & y1 in f.x1 & x2 in dom f & y2 in f.x2
implies (x1,x2)-->(y1,y2) in sproduct f
proof
let x1,x2,y1,y2 be set;
assume that
A1: x1 in dom f and
A2: y1 in f.x1;
A3: x1 .--> y1 in sproduct f by A1,A2,Th60;
assume that
A4: x2 in dom f and
A5: y2 in f.x2;
A6: x2 .--> y2 in sproduct f by A4,A5,Th60;
(x1,x2)-->(y1,y2) = (x1 .--> y1) +* (x2 .--> y2) by FUNCT_4:def 4;
hence thesis by A3,A6,Th70;
end;
begin :: from PRALG_2, 2007.11.14, A.T.
definition
let IT be set;
attr IT is with_common_domain means
:Def10:
for f,g be Function st f in IT & g in IT holds dom f = dom g;
end;
registration
cluster with_common_domain functional non empty for set;
existence
proof
set h = the Function;
take A = {h};
for f,g be Function st f in A & g in A holds dom f = dom g
proof
let f,g be Function;
assume that
A1: f in A and
A2: g in A;
f = h by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
hence A is with_common_domain;
thus A is functional;
thus thesis;
end;
end;
registration
let f;
cluster {f} -> with_common_domain;
coherence
proof
let g,h be Function;
assume g in {f};
then g = f by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
end;
definition
let X be functional set;
func DOM X -> set equals
meet the set of all dom f where f is Element of X;
coherence;
end;
Lm2: for X being functional with_common_domain set
for f being Function st f in X holds dom f = DOM X
proof let X be functional with_common_domain set;
set A = the set of all dom f where f is Element of X;
let f be Function;
assume
A1: f in X;
then dom f in A;
then
A2: { dom f } c= A by ZFMISC_1:31;
A c= { dom f }
proof let e be object;
assume e in A;
then consider g being Element of X such that
A3: e = dom g;
e = dom f by A3,Def10,A1;
hence e in { dom f } by TARSKI:def 1;
end;
then A = { dom f } by A2;
hence dom f = DOM X by SETFAM_1:10;
end;
theorem Th72:
for X be with_common_domain functional set st X = {{}} holds DOM X = {}
proof
let X be with_common_domain functional set;
assume
A1: X = {{}};
{} in {{}} by TARSKI:def 1;
hence thesis by A1,Lm2,RELAT_1:38;
end;
registration let X be empty set;
cluster DOM X -> empty;
coherence
proof set A = the set of all dom f where f is Element of X;
A1: A c= {{}}
proof let e be object;
assume e in A;
then ex f being Element of X st e = dom f;
then e = dom {} by SUBSET_1:def 1;
hence thesis by TARSKI:def 1;
end;
{{}} c= A
proof let e be object;
assume e in {{}};
then e = {} by TARSKI:def 1;
then e = dom {};
then e = dom the Element of X by SUBSET_1:def 1;
hence thesis;
end;
then A = {{}} by A1;
hence thesis by SETFAM_1:10;
end;
end;
begin :: Product like sets, from AMISTD_2, 2007.11.14, A.T.
definition
let S be functional set;
func product" S -> Function means :: tu trzeba uzyc DOM
:Def12: dom it = DOM S &
for i being set st i in dom it holds it.i = pi(S,i);
existence
proof
per cases;
suppose
A1: S = {};
take {};
thus thesis by A1;
end;
suppose
S <> {};
then reconsider S1 = S as non empty functional set;
set D = the set of all dom f where f is Element of S1;
defpred P[object,object] means
ex A being set st A = $1 & $2 = pi(S,A);
A2: for e being object st e in meet D ex u being object st P[e,u]
proof let e be object;
reconsider A = e as set by TARSKI:1;
assume e in meet D;
take u = pi(S,A);
thus thesis;
end;
consider g being Function such that
A3: dom g = meet D and
A4: for e being object st e in meet D holds P[e,g.e]
from CLASSES1:sch 1(A2);
take g;
thus dom g = DOM S by A3;
let i be set;
assume i in dom g;
then P[i,g.i] by A3,A4;
hence thesis;
end;
end;
uniqueness
proof
let f, g be Function such that
A5: dom f = DOM S and
A6: for i being set st i in dom f holds f.i = pi(S,i) and
A7: dom g = DOM S and
A8: for i being set st i in dom g holds g.i = pi(S,i);
for x being object st x in dom f holds f.x = g.x
proof let x be object;
assume
A9: x in dom f;
hence f.x = pi(S,x) by A6 .= g.x by A5,A7,A9,A8;
end;
hence f = g by A5,A7;
end;
end;
::$CT
theorem Th73:
for S being non empty functional set,
i being set st i in dom product" S holds
(product" S).i = the set of all f.i where f is Element of S
proof
let S be non empty functional set, i be set;
assume
A1: i in dom product" S;
hereby
let x be object;
assume x in (product" S).i;
then x in pi(S,i) by A1,Def12;
then ex f being Function st f in S & x = f.i by Def6;
hence x in the set of all f.i where f is Element of S;
end;
let x be object;
assume x in the set of all f.i where f is Element of S;
then ex f being Element of S st x = f.i;
then x in pi(S,i) by Def6;
hence thesis by A1,Def12;
end;
definition
let S be set;
attr S is product-like means
:Def13:
ex f being Function st S = product f;
end;
registration
let f be Function;
cluster product f -> product-like;
coherence;
end;
registration
cluster product-like -> functional with_common_domain for set;
coherence
proof
let S be set;
given f being Function such that
A1: S = product f;
thus S is functional by A1;
let h, g be Function such that
A2: h in S and
A3: g in S;
thus dom h = dom f by A1,A2,Th9
.= dom g by A1,A3,Th9;
end;
end;
registration
cluster product-like non empty for set;
existence
proof
set B = the with_non-empty_elements set,f = the Function of 0,B;
take product f;
thus thesis;
end;
end;
::$CT 2
theorem Th74:
for S being functional with_common_domain set holds S c= product product" S
proof
let S be functional with_common_domain set;
let f be object;
assume
A1: f in S;
then reconsider f as Element of S;
A2: dom f = DOM S by A1,Lm2
.= dom product" S by Def12;
for i being object st i in dom product" S holds f.i in (product" S).i
proof
let i be object;
assume i in dom product" S;
then (product" S).i = pi(S,i) by Def12;
hence thesis by A1,Def6;
end;
hence thesis by A2,Th9;
end;
theorem
for S being non empty product-like set holds S = product product" S
proof
let S be non empty product-like set;
thus S c= product product" S by Th74;
let x be object;
assume x in product product" S;
then consider g being Function such that
A1: x = g and
A2: dom g = dom product" S and
A3: for z being object st z in dom product" S holds g.z in (product" S).z
by Def5;
consider p being Function such that
A4: S = product p by Def13;
set s = the Element of S;
A5: dom g = DOM S by A2,Def12
.= dom s by Lm2
.= dom p by A4,Th9;
for z being object st z in dom p holds g.z in p.z
proof
let z be object;
assume
A6: z in dom p;
then g.z in (product" S).z by A2,A3,A5;
then g.z in pi(S,z) by A2,A5,A6,Def12;
then ex f being Function st f in S & g.z = f.z by Def6;
hence thesis by A4,A6,Th9;
end;
hence thesis by A1,A4,A5,Th9;
end;
:: from AMI_1, 2008.04.11, A.T. (generalized)
theorem
for f being Function
for s, t being Element of product f, A be set holds
s +* t|A is Element of product f
proof
let f be Function;
let s, t be Element of product f, A be set;
per cases;
suppose f is non-empty;
then product f <> {};
then
A1: t in product f;
product f c= sproduct f by Th51;
hence thesis by A1,Th53,Th65;
end;
suppose f is not non-empty;
then {} in rng f;
then
A2: product f = {} by Th26;
t = {} by A2,SUBSET_1:def 1;
then t|A = {};
hence thesis;
end;
end;
theorem
for f being non-empty Function
for p being Element of sproduct f
ex s being Element of product f st p c= s
proof
let f be non-empty Function,
p be Element of sproduct f;
set h = the Element of product f;
reconsider s = h +* p as Element of product f by Th53;
take s;
thus thesis by FUNCT_4:25;
end;
theorem Th78:
g in product f implies g|A in sproduct f
proof
A1: product f c= sproduct f by Th51;
assume g in product f;
hence thesis by A1,Th64,RELAT_1:59;
end;
:: needed, 2008.04.20, A.T.
definition
let f be non-empty Function;
let g be Element of product f;
let X;
redefine func g|X -> Element of sproduct f; :: redefines | (RELAT_1, definition)
coherence by Th78;
end;
theorem
for f being non-empty Function
for s,ss being Element of product f, A being set
holds (ss +* s | A) | A = s | A
proof
let f be non-empty Function;
let s,ss be Element of product f;
let A be set;
dom s = dom f by Th9
.= dom ss by Th9;
then A /\ dom ss c= A /\ dom s;
hence thesis by FUNCT_4:88;
end;
:: from PRE_CIRC, 2008.06.02, A.T.
theorem
for M,x, g being Function st x in product M holds x * g in product (M * g)
proof
let M, x, g be Function;
assume
A1: x in product M;
set xg = x * g;
set Mg = M * g;
A2: ex gg being Function st ( x = gg)&( dom gg = dom M)&( for x
being object st x in dom M holds gg.x in M.x) by A1,Def5;
then
A3: dom xg = dom Mg by RELAT_1:163;
now
let y be object;
assume
A4: y in dom Mg;
then
A5: y in dom g by FUNCT_1:11;
A6: g.y in dom M by A4,FUNCT_1:11;
A7: xg.y = x.(g.y) by A5,FUNCT_1:13;
Mg.y = M.(g.y) by A5,FUNCT_1:13;
hence xg.y in Mg.y by A2,A6,A7;
end;
hence thesis by A3,Def5;
end;
:: moved from CARD_4, 2008.10.08, A.T.
theorem
X is finite iff card X in omega by Th42;
reserve A,B for Ordinal;
theorem Th82:
A is infinite iff omega c= A
proof omega c= A iff not A in omega by ORDINAL1:16;
hence thesis;
end;
theorem
N is finite & not M is finite implies N in M & N c= M
proof
assume that
A1: N is finite and
A2: not M is finite;
A3: N in omega by A1,CARD_1:61;
omega c= M by A2,Th82;
hence N in M by A3;
thus thesis by A1,A2;
end;
theorem
not X is finite iff ex Y st Y c= X & card Y = omega
proof
thus not X is finite implies ex Y st Y c= X & card Y = omega
proof
assume not X is finite;
then not card X in omega;
then
A1: omega c= card X by CARD_1:4;
card X,X are_equipotent by CARD_1:def 2;
then consider f such that
A2: f is one-to-one and
A3: dom f = card X and
A4: rng f = X;
take Y = f.:(omega);
thus Y c= X by A4,RELAT_1:111;
omega,Y are_equipotent
proof
take f|(omega);
thus thesis by A1,A2,A3,FUNCT_1:52,RELAT_1:62,115;
end;
hence thesis by CARD_1:def 2;
end;
given Y such that
A5: Y c= X and
A6: card Y = omega;
thus thesis by A5,A6;
end;
theorem Th85:
card X = card Y iff nextcard X = nextcard Y
proof
thus card X = card Y implies nextcard X = nextcard Y by CARD_1:16;
assume that
A1: nextcard X = nextcard Y and
A2: card X <> card Y;
card X in card Y or card Y in card X by A2,ORDINAL1:14;
then nextcard X c= card Y & card Y in nextcard Y or
nextcard Y c= card X & card X in nextcard X by CARD_1:def 3;
hence thesis by A1,ORDINAL1:12;
end;
theorem
nextcard N = nextcard M implies M = N
proof
A1: card N = N;
card M = M;
hence thesis by A1,Th85;
end;
theorem Th87:
N in M iff nextcard N c= M
proof
A1: N in nextcard N by CARD_1:18;
card N = N;
hence thesis by A1,CARD_1:def 3;
end;
theorem
N in nextcard M iff N c= M
proof
A1: not N c= M iff M in N by CARD_1:4;
N in nextcard M iff not nextcard M c= N by CARD_1:4;
hence thesis by A1,Th87;
end;
theorem
M is finite & (N c= M or N in M) implies N is finite
proof
assume that
A1: M is finite and
A2: N c= M or N in M;
N c= M by A2,CARD_1:3;
hence thesis by A1;
end;
reserve n,k for Nat;
definition
let X;
attr X is countable means
: Def14:
card X c= omega;
attr X is denumerable means
card X = omega;
end;
registration
cluster denumerable -> countable infinite for set;
coherence;
cluster countable infinite -> denumerable for set;
coherence
proof
let X be set;
assume
A1: card X c= omega;
assume X is infinite;
then omega c= card X by Th82;
hence card X = omega by A1;
end;
end;
registration
cluster finite -> countable for set;
coherence;
end;
registration
cluster omega -> denumerable;
coherence;
end;
registration
cluster denumerable for set;
existence
proof
take omega;
thus thesis;
end;
end;
theorem Th90:
X is countable iff ex f st dom f = omega & X c= rng f
by CARD_1:12,CARD_1:47;
registration
let X be countable set;
cluster -> countable for Subset of X;
coherence
proof
let Y be Subset of X;
A1: card Y c= card X by CARD_1:11;
card X c= omega by Def14;
hence card Y c= omega by A1;
end;
end;
Lm3: Y c= X & X is countable implies Y is countable;
theorem
X is countable implies X /\ Y is countable
by Lm3,XBOOLE_1:17;
theorem
X is countable implies X \ Y is countable;
theorem
for A being non empty countable set
ex f being Function of omega, A st rng f = A
proof
let A be non empty countable set;
consider f being Function such that
A1: dom f = omega and
A2: A c= rng f by Th90;
consider x being object such that
A3: x in A by XBOOLE_0:def 1;
set F = f|(f"A) +* (omega \ f"A --> x);
A4: rng F = A & dom F = omega
proof
A5: f"A c= omega by A1,RELAT_1:132;
A6: dom(f|(f"A)) = omega /\ (f"A) by A1,RELAT_1:61;
per cases;
suppose
A7: omega = f"A;
then
A8: omega \ f"A = {} by XBOOLE_1:37;
then dom(f|(f"A)) /\ dom(omega \ f"A --> x) = {};
then dom(f|(f"A)) misses dom(omega \ f"A --> x);
then F = (f|(f"A)) \/ (omega \ f"A --> x) by FUNCT_4:31;
hence rng F = rng(f|(f"A)) \/ rng(omega \ f"A --> x) by RELAT_1:12
.= rng(f|(f"A)) \/ {} by A8
.= f.:(f"A) by RELAT_1:115
.= A by A2,FUNCT_1:77;
thus
dom F = dom(f|(f"A)) \/ dom(omega \ f"A --> x) by FUNCT_4:def 1
.= dom(f|(f"A)) \/ {} by A8
.= omega by A6,A7;
end;
suppose omega <> f"A; then
A9: omega \ f"A is non empty by A5,XBOOLE_1:37;
dom(omega \ f"A --> x) = omega \ f"A;
then F = (f|(f"A)) \/ (omega \ f"A --> x) by A6,FUNCT_4:31,XBOOLE_1:89;
hence rng F = rng(f|(f"A)) \/ rng(omega \ f"A --> x) by RELAT_1:12
.= rng(f|(f"A)) \/ {x} by A9,FUNCOP_1:8
.= f.:(f"A) \/ {x} by RELAT_1:115
.= A \/ {x} by A2,FUNCT_1:77
.= A by A3,ZFMISC_1:40;
thus
dom F = dom(f|(f"A)) \/ dom(omega \ f"A --> x) by FUNCT_4:def 1
.= omega /\ (f"A) \/ (omega \ f"A) by A6
.= omega by XBOOLE_1:51;
end;
end;
then reconsider F as Function of omega, A by FUNCT_2:def 1,RELSET_1:4;
take F;
thus thesis by A4;
end;
:: from CIRCCOMB, 2009.01.26, A.T.
theorem
for f,g being non-empty Function, x being Element of product f,
y being Element of product g holds x+*y in product (f+*g)
proof
let f,g be non-empty Function, x be Element of product f;
let y be Element of product g;
A1: dom x = dom f by Th9;
A2: dom y = dom g by Th9;
then
A3: dom (x+*y) = dom f \/ dom g by A1,FUNCT_4:def 1;
A4: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
now
let z be object;
assume
A5: z in dom (f+*g);
then z in dom g or not z in dom g & z in dom f by A4,XBOOLE_0:def 3;
then (x+*y).z = x.z & (f+*g).z = f.z & x.z in f.z or
(x+*y).z = y.z & (f+*g).z = g.z & y.z in g.z
by A1,A2,A4,A5,Th9,FUNCT_4:def 1;
hence (x+*y).z in (f+*g).z;
end;
hence thesis by A3,A4,Th9;
end;
theorem
for f,g being non-empty Function
for x being Element of product (f+*g) holds x|dom g in product g
proof
let f,g be non-empty Function;
let x be Element of product (f+*g);
A1: dom x = dom (f+*g) by Th9;
A2: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
then
A3: dom g c= dom x by A1,XBOOLE_1:7;
A4: dom (x|dom g) = dom g by A1,A2,RELAT_1:62,XBOOLE_1:7;
now
let z be object;
assume
A5: z in dom (x|dom g);
then
A6: (x|dom g).z = x.z by FUNCT_1:47;
(f+*g).z = g.z by A4,A5,FUNCT_4:13;
hence (x|dom g).z in g.z by A1,A3,A4,A5,A6,Th9;
end;
hence thesis by A4,Th9;
end;
theorem
for f,g being non-empty Function st f tolerates g
for x being Element of product (f+*g) holds x|dom f in product f
proof
let f,g be non-empty Function such that
A1: f tolerates g;
let x be Element of product (f+*g);
A2: dom x = dom (f+*g) by Th9;
A3: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
then
A4: dom f c= dom x by A2,XBOOLE_1:7;
A5: dom (x|dom f) = dom f by A2,A3,RELAT_1:62,XBOOLE_1:7;
now
let z be object;
assume
A6: z in dom (x|dom f);
then
A7: (x|dom f).z = x.z by FUNCT_1:47;
(f+*g).z = f.z by A1,A5,A6,FUNCT_4:15;
hence (x|dom f).z in f.z by A2,A4,A5,A6,A7,Th9;
end;
hence thesis by A5,Th9;
end;
:: missing, 2009.09.06, A.T.
theorem Th97:
for S being with_common_domain functional set, f be Function
st f in S holds dom f = dom product" S
proof let S be with_common_domain functional set, f be Function such that
A1: f in S;
thus dom f = DOM S by A1,Lm2
.= dom product" S by Def12;
end;
theorem Th98:
for S being functional set, f be Function, i be set
st f in S & i in dom product" S holds f.i in (product" S).i
proof
let S being functional set, F be Function, i be set such that
A1: F in S;
assume i in dom product" S;
then (product" S).i = the set of all f.i where f is Element of S
by A1,Th73;
hence F.i in (product" S).i by A1;
end;
theorem
for S being with_common_domain functional set, f be Function, i be set
st f in S & i in dom f holds f.i in (product" S).i
proof let S be with_common_domain functional set, f be Function, i be set;
assume that
A1: f in S and
A2: i in dom f;
dom f = dom(product" S) by A1,Th97;
hence f.i in (product" S).i by A1,A2,Th98;
end;
:: 2009.09.12, A.T.
registration let X be with_common_domain set;
cluster -> with_common_domain for Subset of X;
coherence
by Def10;
end;
:: from PRALG_3, 2009.09.18, A.T.
definition
let f be Function, x be object;
func proj(f,x) -> Function means
:Def16:
dom it = product f & for y being
Function st y in dom it holds it.y = y.x;
existence
proof
defpred P[object,object] means
for g be Function st $1 = g holds $2 = g.x;
A1: now
let q be object;
assume q in product f;
then reconsider q1 = q as Function;
reconsider y = q1.x as object;
take y;
thus P[q,y];
end;
consider F be Function such that
A2: dom F = product f & for a being object st a in product f holds P[a,F.a]
from CLASSES1:sch 1(A1);
take F;
thus thesis by A2;
end;
uniqueness
proof
let F,G be Function such that
A3: dom F = product f and
A4: for y being Function st y in dom F holds F.y = y.x and
A5: dom G = product f and
A6: for y being Function st y in dom G holds G.y = y.x;
now
let y be object;
assume
A7: y in product f;
then reconsider x1 = y as Function;
thus F.y = x1.x by A3,A4,A7
.= G.y by A5,A6,A7;
end;
hence thesis by A3,A5;
end;
end;
registration
let f be Function, x be object;
cluster proj(f,x) -> (product f)-defined;
coherence
by Def16;
end;
registration
let f be Function, x be object;
cluster proj(f,x) -> total;
coherence
by Def16;
end;
registration
let f be non-empty Function;
cluster -> f-compatible for Element of product f;
coherence
proof let e be Element of product f;
let x be object;
assume x in dom e;
then x in dom f by Th9;
hence e.x in f.x by Th9;
end;
end;
registration
let I be set; let f be I-defined non-empty Function;
cluster -> I-defined for Element of product f;
coherence;
end;
registration
let f be Function;
cluster -> f-compatible for Element of sproduct f;
coherence
by Th49;
end;
registration
let I be set; let f be I-defined Function;
cluster -> I-defined for Element of sproduct f;
coherence;
end;
registration
let I be set; let f be total I-defined non-empty Function;
cluster -> total for Element of product f;
coherence
proof let e be Element of product f;
thus dom e = dom f by Th9
.= I by PARTFUN1:def 2;
end;
end;
theorem Th100:
for I being set, f being non-empty I-defined Function
for p being f-compatible I-defined Function
holds p in sproduct f
proof let I be set, f be non-empty I-defined Function;
let p be f-compatible I-defined Function;
A1: dom p c= dom f by FUNCT_1:105;
for x being object st x in dom p holds p.x in f.x by FUNCT_1:def 14;
hence p in sproduct f by A1,Def9;
end;
theorem
for I being set, f being non-empty I-defined Function
for p being f-compatible I-defined Function
ex s being Element of product f st p c= s
proof let I be set;
let f be non-empty I-defined Function,
p be f-compatible I-defined Function;
reconsider p as Element of sproduct f by Th100;
set h = the Element of product f;
reconsider s = h +* p as Element of product f by Th53;
take s;
thus thesis by FUNCT_4:25;
end;
:: from AMISTD_2, 2010.01.10, A.T
registration
let X be infinite set, a be set;
cluster X --> a -> infinite;
coherence;
end;
registration
cluster infinite for Function;
existence
proof
take omega --> 0;
thus thesis;
end;
end;
:: ORDERS_1:86, 2012.10.02, A.T.
Lm4: field R is finite implies R is finite
proof
assume field R is finite;
then reconsider A = field R as finite set;
R c= [:A,A:] :: by Lm4; from ORDERS_1
proof
let y,z be object;
assume
A1: [y,z] in R;
then
A2: z in field R by RELAT_1:15;
y in field R by A1,RELAT_1:15;
hence thesis by A2,ZFMISC_1:87;
end;
hence thesis;
end;
registration
let R be infinite Relation;
cluster field R -> infinite;
coherence by Lm4;
end;
registration
let X be infinite set;
cluster RelIncl X -> infinite;
coherence by CARD_1:63;
end;
theorem
for R,S being Relation st R,S are_isomorphic & R is finite
holds S is finite
proof
let R,S be Relation;
given F being Function such that
A1: F is_isomorphism_of R,S;
assume R is finite;
then field R is finite;
then dom F is finite by A1;
then rng F is finite by FINSET_1:8;
then field S is finite by A1;
hence thesis;
end;
theorem
product" {{}} = {}
proof
dom product" {{}} = DOM {{}} by Def12
.= {} by Th72;
hence thesis;
end;
theorem Th104:
for I being set, f being non-empty ManySortedSet of I
for s being f-compatible ManySortedSet of I
holds s in product f
proof let I be set, f be non-empty ManySortedSet of I;
let s be f-compatible ManySortedSet of I;
A1: dom s = I by PARTFUN1:def 2 .= dom f by PARTFUN1:def 2;
then for x being object st x in dom f holds s.x in f.x by FUNCT_1:def 14;
hence s in product f by A1,Th9;
end;
registration
let I be set, f be non-empty ManySortedSet of I;
cluster -> total for Element of product f;
coherence;
end;
definition
let I be set, f be non-empty ManySortedSet of I;
let M be f-compatible ManySortedSet of I;
func down M -> Element of product f equals M;
coherence by Th104;
end;
theorem
for X being functional with_common_domain set
for f being Function st f in X holds dom f = DOM X by Lm2;
theorem
for x being object, X being non empty functional set
st for f being Function st f in X holds x in dom f
holds x in DOM X
proof let x be object, X be non empty functional set such that
A1: for f being Function st f in X holds x in dom f;
set A = the set of all dom f where f is Element of X;
consider Y being object such that
A2: Y in X by XBOOLE_0:def 1;
reconsider Y as Function by A2;
A3: dom Y in A by A2;
for Y holds Y in A implies x in Y
proof let Y;
assume Y in A;
then ex f being Element of X st Y = dom f;
hence x in Y by A1;
end;
hence x in DOM X by A3,SETFAM_1:def 1;
end;
scheme FuncSepOrg { X()->set, F(object)->set, P[object,object] }:
ex f st dom f = X() &
for x being set st x in X()
for y being set holds y in f.x iff y in F(x) & P[x,y]
proof
consider f such that
A1: dom f = X() and
A2: for x being object st x in X()
for y being object holds y in f.x iff y in F(x) & P[x,y]
from FuncSeparation;
take f;
thus thesis by A1,A2;
end;
:: from NAGATA_1, 2013.01.13, A.T.
notation
let X be set;
antonym X is uncountable for X is countable;
end;
registration
cluster uncountable -> non empty for set;
coherence;
end;