:: Function Domains and Fr{\ae}nkel Operator
:: by Andrzej Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990-2021 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 XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, FUNCT_2, ZFMISC_1,
PARTFUN1, FINSET_1, MCART_1, FINSUB_1, SETWISEO;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
FINSET_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
DOMAIN_1, SETWISEO;
constructors PARTFUN1, BINOP_1, DOMAIN_1, FINSET_1, SETWISEO, RELSET_1,
XTUPLE_0;
registrations SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, BINOP_1;
expansions TARSKI, XBOOLE_0;
theorems FINSET_1, ZFMISC_1, MCART_1, FUNCT_1, FUNCT_2, FINSUB_1, RELAT_1,
RELSET_1, XBOOLE_0, XBOOLE_1, TARSKI, SUBSET_1;
schemes FUNCT_1, FUNCT_2, SETWISEO, DOMAIN_1, PARTFUN1;
begin
reserve B for non empty set,
A,X,x for set;
scheme
Fraenkel59{ A() -> set, F(object) -> object, P,Q[object] } :
{ F(v) where v is Element of A() : P[v] } c=
{ F(u) where u is Element of A() : Q[u] }
provided
A1: for v being Element of A() holds P[v] implies Q[v]
proof
let x be object;
assume x in { F(v9) where v9 is Element of A() : P[v9] };
then consider v being Element of A() such that
A2: x = F(v) and
A3: P[v];
Q[v] by A1,A3;
hence thesis by A2;
end;
scheme
Fraenkel599 { A,B() -> set, F(object,object) -> object, P,Q[object,object] }:
{ F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } c=
{ F(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] }
provided
A1: for u being (Element of A()), v being Element of B() holds P[u,v]
implies Q[u,v]
proof
let x be object;
assume x in {F(u9,v9) where u9 is (Element of A()), v9 is Element of B() :
P[u9,v9]};
then consider u being (Element of A()), v being Element of B() such that
A2: x = F(u,v) and
A3: P[u,v];
Q[u,v] by A1,A3;
hence thesis by A2;
end;
scheme
Fraenkel69{ B() -> set, F(object) -> object, P, Q[object] } :
{ F(v1) where v1 is Element of B() : P[v1] } =
{ F(v2) where v2 is Element of B() : Q[v2] }
provided
A1: for v being Element of B() holds P[v] iff Q[v]
proof
set A = { F(v1) where v1 is Element of B() : P[v1] }, B = { F(v2) where v2
is Element of B() : Q[v2] };
A2: for v being Element of B() holds P[v] implies Q[v] by A1;
thus A c= B from Fraenkel59(A2);
A3: for v being Element of B() holds Q[v] implies P[v] by A1;
thus B c= A from Fraenkel59(A3);
end;
scheme
Fraenkel699 { A,B() -> set, F(object,object) -> object, P,Q[object,object] }:
{ F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } =
{ F(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] }
provided
A1: for u being Element of A(), v being Element of B() holds P[u,v]
iff Q[u,v]
proof
set B = { F(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2
,v2] };
set A = { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1
,v1] };
A2: for u being (Element of A()), v being Element of B() holds P[u,v]
implies Q[u,v] by A1;
thus A c= B from Fraenkel599(A2);
A3: for u being (Element of A()), v being Element of B() holds Q[u,v]
implies P[u,v] by A1;
thus B c= A from Fraenkel599(A3);
end;
scheme
FraenkelF9{ B() -> set, F,G(object) -> object, P[object] } :
{ F(v1) where v1 is Element of B() : P[v1] } =
{ G(v2) where v2 is Element of B() : P[v2] }
provided
A1: for v being Element of B() holds F(v) = G(v)
proof
set X = { F(v1) where v1 is Element of B() : P[v1] }, Y = { G(v2) where v2
is Element of B() : P[v2] };
A2: Y c= X
proof
let x be object;
assume x in Y;
then consider v1 being Element of B() such that
A3: x = G(v1) and
A4: P[v1];
x = F(v1) by A1,A3;
hence thesis by A4;
end;
X c= Y
proof
let x be object;
assume x in X;
then consider v1 being Element of B() such that
A5: x = F(v1) and
A6: P[v1];
x = G(v1) by A1,A5;
hence thesis by A6;
end;
hence thesis by A2;
end;
scheme
FraenkelF9R{ B() -> set, F,G(object) -> object, P[object] } :
{ F(v1) where v1 is Element of B() : P[v1] } =
{ G(v2) where v2 is Element of B() : P[v2] }
provided
A1: for v being Element of B() st P[v] holds F(v) = G(v)
proof
set X = { F(v1) where v1 is Element of B() : P[v1] }, Y = { G(v2) where v2
is Element of B() : P[v2] };
A2: Y c= X
proof
let x be object;
assume x in Y;
then consider v1 being Element of B() such that
A3: x = G(v1) and
A4: P[v1];
x = F(v1) by A1,A3,A4;
hence thesis by A4;
end;
X c= Y
proof
let x be object;
assume x in X;
then consider v1 being Element of B() such that
A5: x = F(v1) and
A6: P[v1];
x = G(v1) by A1,A5,A6;
hence thesis by A6;
end;
hence thesis by A2;
end;
scheme
FraenkelF99 { A,B() -> set, F,G(object,object) -> object, P[object,object] }:
{ F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } =
{ G(u2,v2) where u2 is Element of A(), v2 is Element of B() : P[u2,v2] }
provided
A1: for u being Element of A(), v being Element of B() holds F(u,v) = G(u,v)
proof
set Y = { G(u2,v2) where u2 is (Element of A()), v2 is Element of B() : P[u2
,v2] };
set X = { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1
,v1] };
A2: Y c= X
proof
let x be object;
assume x in Y;
then consider u1 being (Element of A()), v1 being Element of B() such that
A3: x = G(u1,v1) and
A4: P[u1,v1];
x = F(u1,v1) by A1,A3;
hence thesis by A4;
end;
X c= Y
proof
let x be object;
assume x in X;
then consider u1 being (Element of A()), v1 being Element of B() such that
A5: x = F(u1,v1) and
A6: P[u1,v1];
x = G(u1,v1) by A1,A5;
hence thesis by A6;
end;
hence thesis by A2;
end;
scheme
FraenkelF699 { A,B() -> set, F(object,object) -> object,
P,Q[object,object] }:
{ F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } =
{ F(v2,u2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] }
provided
A1: for u being Element of A(), v being Element of B() holds P[u,v]
iff Q[u,v] and
A2: for u being Element of A(), v being Element of B() holds F(u,v) = F(v,u)
proof
A3: for u being Element of A(), v being Element of B() holds Q[u,v]
implies P[u,v] by A1;
A4: { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : Q[u1,v1]
} c= { F(u2,v2) where u2 is (Element of A()), v2 is Element of B() : P[u2,v2] }
from Fraenkel599(A3);
deffunc H(set,set) = F($2,$1);
A5: for u being (Element of A()), v being Element of B() holds P[u,v]
implies Q[u,v] by A1;
A6: { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1,v1]
} c= { F(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2,v2] }
from Fraenkel599(A5);
A7: for u being Element of A(), v being Element of B() holds F(u,v) = H(u,v)
by A2;
{ F(u1,v1) where u1 is Element of A(), v1 is Element of B() : Q[u1,v1] }
= { H(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] } from
FraenkelF99(A7);
hence thesis by A6,A4;
end;
theorem Th1:
for A,B being set, F,G being Function of A,B for X
being set st F|X = G|X for x being Element of A st x in X holds F.x = G.x
proof
let A,B be set, F,G be Function of A,B;
let X be set such that
A1: F|X = G|X;
let x be Element of A;
assume
A2: x in X;
hence F.x = (G|X).x by A1,FUNCT_1:49
.= G.x by A2,FUNCT_1:49;
end;
theorem Th2:
for A,B being set holds Funcs(A,B) c= bool [:A,B:]
proof
let A,B be set, x be object;
assume x in Funcs(A,B);
then consider f being Function such that
A1: x = f and
A2: dom f = A and
A3: rng f c= B by FUNCT_2:def 2;
A4: f c= [: dom f, rng f:] by RELAT_1:7;
[:dom f, rng f:] c= [:A,B:] by A2,A3,ZFMISC_1:95;
then f c= [:A,B:] by A4;
hence thesis by A1;
end;
theorem Th3:
for X,Y being set st Funcs(X,Y) <> {} & X c= A & Y c= B for f
being Element of Funcs(X,Y) holds f is PartFunc of A,B
proof
let X,Y be set such that
A1: Funcs(X,Y) <> {} and
A2: X c= A and
A3: Y c= B;
let f be Element of Funcs(X,Y);
consider g being Function such that
A4: f = g and
A5: dom g = X and
A6: rng g c= Y by A1,FUNCT_2:def 2;
rng g c= B by A3,A6;
hence thesis by A2,A4,A5,RELSET_1:4;
end;
scheme
RelevantArgs
{ A,B,X() -> set, f,g() -> Function of A(),B(), P,Q[object] } :
{ f().u9 where u9 is Element of A() : P[u9] & u9 in X() } =
{ g().v9 where v9 is Element of A() : Q[v9] & v9 in X() }
provided
A1: f()|X() = g()|X() and
A2: for u being Element of A() st u in X() holds P[u] iff Q[u]
proof
deffunc F(set) = f().$1;
deffunc G(set) = g().$1;
defpred PP[set] means P[$1] & $1 in X();
defpred QQ[set] means Q[$1] & $1 in X();
set C = { G(v9) where v9 is Element of A() : PP[v9] };
A3: for v being Element of A() holds PP[v] iff QQ[v] by A2;
A4: C = { G(v9) where v9 is Element of A() : QQ[v9] } from Fraenkel69(A3);
A5: for v being Element of A() st PP[v] holds F(v) = G(v) by A1,Th1;
{ F(u9) where u9 is Element of A() : PP[u9] } = C from FraenkelF9R(A5);
hence thesis by A4;
end;
scheme
FrSet0{ A() -> non empty set, P[object] }:
{ x where x is Element of A(): P[x] } c= A()
proof
{ x where x is Element of A(): P[x] } is Subset of A() from DOMAIN_1:sch 7;
hence thesis;
end;
scheme
Gen199{A,B() -> set, F(object,object) -> object, P[object,object],
Q[object] }:
for s being Element of A(), t being Element of B() st P[s,t] holds Q[F(s,t)]
provided
A1: for st1 being set st st1 in { F(s1,t1) where s1 is (Element of A()),
t1 is Element of B(): P[s1,t1] } holds Q[st1]
proof
let s be (Element of A()), t be Element of B();
assume P[s,t];
then
F(s,t) in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B():
P[s1,t1] };
hence thesis by A1;
end;
scheme
Gen199A{A,B() -> set, F(object,object) -> object, P[object,object],
Q[object] } :
for st1 being set st st1 in { F(s1,t1) where s1 is Element of A(),
t1 is Element of B(): P[s1,t1] } holds Q[st1]
provided
A1: for s being Element of A(), t being Element of B() st P[s,t] holds
Q[F(s,t)]
proof
let st1 be set;
assume st1 in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B()
: P[s1,t1] };
then
ex s1 being (Element of A()), t1 being Element of B() st st1 = F(s1,t1)
& P[s1,t1];
hence thesis by A1;
end;
scheme
Gen299{A,B,C() -> set, F(object,object) -> Element of C(), P[object,object],
Q[object] } :
{ st1 where st1 is Element of C() :
st1 in { F(s1,t1) where s1 is Element of A(), t1 is Element of B() :
P[s1,t1] } & Q[st1] } =
{ F(s2,t2) where s2 is Element of A(), t2 is Element of B() :
P[s2,t2] & Q[F(s2,t2)]}
proof
thus { st1 where st1 is Element of C() : st1 in { F(s1,t1) where s1 is (
Element of A()), t1 is Element of B() : P[s1,t1] } & Q[st1] } c= { F(s2,t2)
where s2 is (Element of A()), t2 is Element of B() : P[s2,t2] & Q[F(s2,t2)]}
proof
let x be object;
assume x in { st1 where st1 is Element of C() : st1 in { F(s1,t1) where
s1 is (Element of A()), t1 is Element of B() : P[s1,t1] } & Q[st1] };
then consider st1 being Element of C() such that
A1: x = st1 and
A2: st1 in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B
() : P[s1,t1] } and
A3: Q[st1];
ex s1 being (Element of A()), t1 being Element of B() st st1 = F(s1,t1
) & P[s1,t1] by A2;
hence thesis by A1,A3;
end;
let x be object;
assume x in { F(s2,t2) where s2 is (Element of A()), t2 is Element of B() :
P[s2,t2] & Q[F(s2,t2)]};
then consider s2 being (Element of A()), t2 being Element of B() such that
A4: x = F(s2,t2) and
A5: P[s2,t2] and
A6: Q[F(s2,t2)];
F(s2,t2) in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B
( ) : P[s1,t1] } by A5;
hence thesis by A4,A6;
end;
scheme
Gen39{A() -> set, F(object) -> object, P,Q[object] } :
{ F(s) where s is Element of A() :
s in { s1 where s1 is Element of A(): Q[s1] } & P[s] } = {
F(s2) where s2 is Element of A() : Q[s2] & P[s2] } proof
defpred QQ[set] means Q[$1] & P[$1];
defpred PP[set] means $1 in { s1 where s1 is Element of A(): Q[s1] } & P[$1];
A1: for s being Element of A() holds PP[s] iff QQ[s]
proof
let s be Element of A();
now
assume s in { s1 where s1 is Element of A(): Q[s1] };
then ex s1 being Element of A() st s = s1 & Q[s1];
hence Q[s];
end;
hence thesis;
end;
thus { F(s) where s is Element of A() : PP[s] } = { F(s2) where s2 is
Element of A() : QQ[s2] } from Fraenkel69(A1);
end;
scheme
Gen399{A,B() -> set, F(object,object) -> object, P[object,object],
Q[object] }:
{ F(s,t) where s is (Element of A()), t is Element of B() : s
in { s1 where s1 is Element of A(): Q[s1] } & P[s,t] } = { F(s2,t2) where s2 is
(Element of A()), t2 is Element of B() : Q[s2] & P[s2,t2] } proof
defpred QQ[set,set] means Q[$1] & P[$1,$2];
defpred PP[set,set] means $1 in { s1 where s1 is Element of A(): Q[s1] } & P
[$1,$2];
A1: for s being Element of A(), t being Element of B() holds PP[s,t] iff QQ[
s,t]
proof
let s be Element of A(), t be Element of B();
now
assume s in { s1 where s1 is Element of A(): Q[s1] };
then ex s1 being Element of A() st s = s1 & Q[s1];
hence Q[s];
end;
hence thesis;
end;
thus { F(s,t) where s is (Element of A()), t is Element of B() : PP[s,t] } =
{ F(s2,t2) where s2 is (Element of A()), t2 is Element of B() : QQ[s2,t2] }
from Fraenkel699(A1);
end;
scheme
Gen499{A,B() -> set, F(object,object) -> object, P,Q[object,object] } :
{ F(s,t) where s is (Element of A()), t is Element of B()
: P[s,t] } c= { F(s1,t1) where s1 is (Element of A()), t1 is Element of B() : Q
[s1,t1] }
provided
A1: for s being (Element of A()), t being Element of B() st P[s,t] ex s9
being Element of A() st Q[s9,t] & F(s,t) = F(s9,t)
proof
let x be object;
assume
x in { F(s,t) where s is (Element of A()), t is Element of B() : P[s ,t] };
then consider s being (Element of A()), t being Element of B() such that
A2: x = F(s,t) and
A3: P[s,t];
ex s9 being Element of A() st Q[s9,t] & F(s,t) = F(s9,t) by A1,A3;
hence thesis by A2;
end;
scheme
FrSet1{ D,A() -> set, P[object], F(object) -> object }:
{ F(y) where y is Element of D() : F(y) in A() & P[y] } c= A()
proof
let x be object;
assume x in { F(y) where y is Element of D() : F(y) in A() & P[y] };
then ex y being Element of D() st x = F(y) & F(y) in A() & P[y];
hence thesis;
end;
scheme
FrSet2{ D,A() -> set, Q[object], F(object) -> object }:
{ F(y) where y is Element of D() : Q[y] & not F(y) in A() } misses A()
proof
assume
{ F(y) where y is Element of D() : Q[y] & not F(y) in A() } meets A( );
then consider x be object such that
A1: x in { F(y) where y is Element of D() : Q[y] & not F(y) in A() } and
A2: x in A() by XBOOLE_0:3;
ex y being Element of D() st x = F(y) & Q[y] & not F(y) in A() by A1;
hence thesis by A2;
end;
scheme
FrEqua1{ A,B() -> set, F(object,object) -> object, x() -> (Element of B()),
P,Q[object,object] }: { F(s,t) where s is (Element of
A()), t is Element of B(): Q[s,t] } = { F(s9,x()) where s9 is Element of A(): P
[s9,x()] }
provided
A1: for s being Element of A() for t being Element of B() holds Q[s,t]
iff t = x() & P[s,t]
proof
thus { F(s,t) where s is (Element of A()), t is Element of B(): Q[s,t] } c=
{ F(s9,x()) where s9 is Element of A(): P[s9,x()] }
proof
let x be object;
assume
x in { F(s,t) where s is (Element of A()), t is Element of B(): Q[ s,t ] };
then consider s being (Element of A()), t being Element of B() such that
A2: x = F(s,t) and
A3: Q[s,t];
A4: P[s,t] by A1,A3;
t = x() by A1,A3;
hence thesis by A2,A4;
end;
let x be object;
assume x in { F(s9,x()) where s9 is Element of A(): P[s9,x()] };
then consider s9 being Element of A() such that
A5: x = F(s9,x()) and
A6: P[s9,x()];
Q[s9,x()] by A1,A6;
hence thesis by A5;
end;
scheme
FrEqua2{ A,B() -> set, F(object,object) -> object, x() -> (Element of B()),
P[object,object] }: { F(s,t) where s is (Element of A()), t is
Element of B(): t = x() & P[s,t] } = { F(s9,x()) where s9 is Element of A(): P[
s9,x()] } proof
defpred Q[set,set] means $2 = x() & P[$1,$2];
A1: for s being Element of A() for t being Element of B() holds Q[s,t] iff t
= x() & P[s,t];
thus { F(s,t) where s is Element of A(), t is Element of B(): Q[s,t] } = { F
(s9,x()) where s9 is Element of A(): P[s9,x()] } from FrEqua1(A1);
end;
:: dziedziny funkcji
reserve phi for Element of Funcs(A,B);
theorem Th4:
for X,Y being set st Funcs(X,Y) <> {} & X c= A & Y c= B for f
being Element of Funcs(X,Y) ex phi being Element of Funcs(A,B) st phi|X = f
proof
let X,Y be set such that
A1: Funcs(X,Y) <> {} and
A2: X c= A and
A3: Y c= B;
let f be Element of Funcs(X,Y);
reconsider f9=f as PartFunc of A,B by A1,A2,A3,Th3;
consider phi being Function of A,B such that
A4: for x being object st x in dom f9 holds phi.x = f9.x by FUNCT_2:71;
reconsider phi as Element of Funcs(A,B) by FUNCT_2:8;
take phi;
ex g being Function st f = g & dom g = X & rng g c= Y by A1,FUNCT_2:def 2;
then dom f9 = A /\ X by XBOOLE_1:28
.= dom phi /\ X by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:46;
end;
theorem Th5:
phi|X = phi|(A /\ X)
proof
dom phi = A by FUNCT_2:def 1;
then
A1: dom (phi|X) = (dom phi /\ A) /\ X by RELAT_1:61
.= dom phi /\ (A /\ X) by XBOOLE_1:16;
for x being object st x in dom (phi|X) holds (phi|X).x = phi.x by
FUNCT_1:47;
hence thesis by A1,FUNCT_1:46;
end;
:: Zbiory skonczone
scheme
FraenkelFin { A,X() -> set, F(object) -> object }:
{ F(w) where w is Element of A(): w in X() } is finite
provided
A1: X() is finite
proof
set M = { F(w) where w is Element of A(): w in X() };
per cases;
suppose
A2: A() is empty;
M c= {F({})}
proof
let x be object;
assume x in M;
then consider w being Element of A() such that
A3: x = F(w) & w in X();
w = {} by A2,SUBSET_1:def 1;
hence thesis by A3,TARSKI:def 1;
end;
hence thesis;
end;
suppose
A4: A() is non empty;
consider f being Function such that
A5: dom f = X() /\ A() and
A6: for y being object st y in X() /\ A() holds f.y = F(y) from FUNCT_1:sch 3;
M = f.:X()
proof
thus M c= f.:X()
proof
let x be object;
assume x in M;
then consider u being Element of A() such that
A7: x = F(u) and
A8: u in X();
A9: u in dom f by A4,A5,A8,XBOOLE_0:def 4;
then f.u = F(u) by A5,A6;
hence thesis by A7,A8,A9,FUNCT_1:def 6;
end;
let x be object;
assume x in f.:X();
then consider y being object such that
A10: y in dom f and
A11: y in X() and
A12: x = f.y by FUNCT_1:def 6;
reconsider y as Element of A() by A5,A10,XBOOLE_0:def 4;
x = F(y) by A5,A6,A10,A12;
hence thesis by A11;
end;
hence thesis by A1;
end;
end;
scheme
CartFin { A, B() -> non empty set, X, Y() -> set,
F(object, object) -> object }:
{ F(u,v) where u is Element of A(), v is Element of B() :
u in X() & v in Y () } is finite
provided
A1: X() is finite and
A2: Y() is finite
proof
deffunc G(object) = F($1`1,$1`2);
set M = { F(u9,v9) where u9 is (Element of A()), v9 is Element of B() : u9
in X() & v9 in Y() };
consider f being Function such that
A3: dom f = [:X() /\ A(), Y() /\ B():] and
A4: for y being object st y in [:X() /\ A(), Y() /\ B():] holds f.y = G(y)
from FUNCT_1:sch 3;
A5: dom f = [:X(), Y():] /\ [:A(), B():] by A3,ZFMISC_1:100;
M = f.:[:X(), Y():]
proof
thus M c= f.:[:X(), Y():]
proof
let x be object;
assume x in M;
then consider u being Element of A(), v being Element of B() such that
A6: x = F(u,v) and
A7: u in X() and
A8: v in Y();
A9: [u,v] in [:X(), Y():] by A7,A8,ZFMISC_1:87;
then
A10: [u,v] in dom f by A5,XBOOLE_0:def 4;
A11: [u,v]`2 = v;
[u,v]`1 = u;
then f.(u,v) = F(u,v) by A3,A4,A10,A11;
hence thesis by A6,A9,A10,FUNCT_1:def 6;
end;
let x be object;
assume x in f.:[:X(), Y():];
then consider y being object such that
A12: y in dom f and
A13: y in [:X(), Y():] and
A14: x = f.y by FUNCT_1:def 6;
reconsider y as Element of [:A(), B():] by A5,A12,XBOOLE_0:def 4;
A15: y = [y`1,y`2] by MCART_1:21;
then
A16: y`1 in X() by A13,ZFMISC_1:87;
A17: y`2 in Y() by A13,A15,ZFMISC_1:87;
x = F(y`1,y`2) by A3,A4,A12,A14;
hence thesis by A16,A17;
end;
hence thesis by A1,A2;
end;
scheme
Finiteness { A()->non empty set, B()->(Element of Fin A()), P[(Element of A(
)), Element of A()] } : for x being Element of A() st x in B() ex y being
Element of A() st y in B() & P[y,x] & for z being Element of A() st z in B() &
P[z,y] holds P[y,z]
provided
A1: for x being Element of A() holds P[x,x] and
A2: for x,y,z being Element of A() st P[x,y] & P[y,z] holds P[x,z]
proof
defpred R[(Element of A()), Element of Fin A()] means ex y being Element of
A() st y in $2 & P[y,$1] & for z being Element of A() st z in $2 & P[z,y] holds
P[y,z];
defpred Q[Element of Fin A()] means for x being Element of A() st x in $1
holds R[x, $1];
A3: now
let B be (Element of Fin A()), x be Element of A();
assume
A4: Q[B];
thus Q[B \/ {.x.}]
proof
let z be Element of A() such that
A5: z in B \/ {x};
now
per cases by A5,ZFMISC_1:136;
suppose
z in B;
then consider y being Element of A() such that
A6: y in B and
A7: P[y,z] and
A8: for x being Element of A() st x in B & P[x,y] holds P[y,x] by A4;
now
per cases;
case
A9: P[x,y];
thus x in B \/ {x} by ZFMISC_1:136;
thus P[x,z] by A2,A7,A9;
let v be Element of A() such that
A10: v in B \/ {x} and
A11: P[v,x];
A12: now
assume
A13: v in B;
P[v,y] by A2,A9,A11;
then P[y,v] by A8,A13;
hence P[x,v] by A2,A9;
end;
v in B or v = x by A10,ZFMISC_1:136;
hence P[x,v] by A1,A12;
end;
case
A14: not P[x,y];
thus y in B \/ {x} by A6,XBOOLE_0:def 3;
thus P[y,z] by A7;
let v be Element of A() such that
A15: v in B \/ {x} and
A16: P[v,y];
v in B or v = x by A15,ZFMISC_1:136;
hence P[y,v] by A8,A14,A16;
end;
end;
hence thesis;
end;
suppose
A17: z = x;
now
per cases;
case
ex w being Element of A() st w in B & P[w,x];
then consider w being Element of A() such that
A18: w in B and
A19: P[w,z] by A17;
consider y being Element of A() such that
A20: y in B and
A21: P[y,w] and
A22: for x being Element of A() st x in B & P[x,y] holds P[y
,x] by A4,A18;
take u = y;
thus u in B \/ {x} by A20,XBOOLE_0:def 3;
thus P[u,z] by A2,A19,A21;
let v be Element of A() such that
A23: v in B \/ {x} and
A24: P[v,u];
v in B or v = x by A23,ZFMISC_1:136;
hence P[u,v] by A2,A17,A19,A21,A22,A24;
end;
case
A25: for w being Element of A() st w in B holds not P[w,x];
thus x in B \/ {x} by ZFMISC_1:136;
thus
A26: P[x,x] by A1;
let v be Element of A() such that
A27: v in B \/ {x} and
A28: P[v,x];
not v in B by A25,A28;
hence P[x,v] by A26,A27,ZFMISC_1:136;
end;
end;
hence thesis by A17;
end;
end;
hence thesis;
end;
end;
A29: Q[{}.A()];
for B being Element of Fin A() holds Q[B] from SETWISEO:sch 4(A29,A3 );
hence thesis;
end;
scheme
FinIm{A,B()->non empty set, x()-> (Element of Fin B()),
F(object)->(Element of A()), P[object,object]}:
ex c1 being Element of Fin A() st for t
being Element of A() holds t in c1 iff ex t9 being Element of B() st t9 in x()
& t = F(t9) & P[t,t9] proof
defpred R[set] means ex t9 being Element of B() st t9 in x() & $1 = F(t9) &
P[$1,t9];
set c = { F(t9) where t9 is Element of B() : t9 in x() }, c1 = { tt where tt
is Element of A() : R[tt]};
A1: c1 c= c
proof
let x be object;
assume x in c1;
then ex tt being Element of A() st x = tt & ex t9 being Element of B() st
t9 in x() & tt = F(t9) & P[tt,t9];
hence thesis;
end;
A2: c1 c= A() from FrSet0;
A3: x() is finite;
c is finite from FraenkelFin(A3);
then reconsider c1 as Element of Fin A() by A1,A2,FINSUB_1:def 5;
take c1;
let t be Element of A();
t in c1 implies ex tt being Element of A() st t = tt & ex t9 being
Element of B() st t9 in x() & tt = F(t9) & P[tt,t9];
hence thesis;
end;
registration
let A, B be finite set;
cluster Funcs(A,B) -> finite;
coherence
proof
bool [:A,B:] is finite;
hence thesis by Th2,FINSET_1:1;
end;
end;
theorem
for A,B being set st A is finite & B is finite holds Funcs(A,B) is finite;
scheme
ImFin { A() -> set, B() -> non empty set, X,Y() -> set,
F(object) -> object } :
{ F(phi9) where phi9 is Element of Funcs(A(),B()): phi9.:X() c= Y() }
is finite
provided
A1: X() is finite and
A2: Y() is finite and
A3: for phi,psi being Element of Funcs(A(),B()) holds phi|X() = psi|X()
implies F(phi) = F(psi)
proof
defpred P[set,set] means for phi being Element of Funcs(A(),B()) st phi|X()
= $1 holds $2 = F(phi);
set Z = { F(phi9) where phi9 is Element of Funcs(A(),B()): phi9.: X() c= Y()
};
set x = the Element of Z;
A4: B() /\ Y() c= B() by XBOOLE_1:17;
assume
A5: not thesis;
then Z <> {};
then x in Z;
then consider phi being Element of Funcs(A(),B()) such that
x = F(phi) and
A6: phi.:X() c= Y();
now
assume B() /\ Y() = {};
then
A7: phi.:X() = {} by A6,XBOOLE_1:3,19;
A() = dom phi by FUNCT_2:def 1;
then A() misses X() by A7,RELAT_1:118;
hence A() /\ X() = {};
end;
then reconsider FF = Funcs(A() /\ X(),B() /\ Y()), Z as non empty set by A5,
FUNCT_2:8;
A8: B() /\ Y() c= Y() by XBOOLE_1:17;
A9: A() /\ X() c= A() by XBOOLE_1:17;
A10: now
let f be Element of FF;
consider phi being Element of Funcs(A(),B()) such that
A11: phi|(A() /\ X()) = f by A9,A4,Th4;
A12: phi|X() = f by A11,Th5;
ex g being Function st f = g & dom g = A() /\ X() & rng g c= B() /\ Y
() by FUNCT_2:def 2;
then rng (phi|X()) c= Y() by A8,A12;
then phi.:X() c= Y() by RELAT_1:115;
then F(phi) in Z;
then reconsider g9 = F(phi) as Element of Z;
take g = g9;
thus P[f,g] by A3,A12;
end;
consider F being Function of FF, Z such that
A13: for f being Element of FF holds P[f,F.f] from FUNCT_2:sch 3(A10);
Z c= F.:Funcs(A() /\ X(), B() /\ Y())
proof
let y be object;
assume y in Z;
then consider phi being Element of Funcs(A(),B()) such that
A14: y = F(phi) and
A15: phi.:X() c= Y();
rng (phi|X()) c= Y() by A15,RELAT_1:115;
then
A16: rng (phi|X()) c= B() /\ Y() by XBOOLE_1:19;
A17: dom (phi|X()) = dom phi /\ X() by RELAT_1:61
.= A() /\ X() by FUNCT_2:def 1;
then reconsider
x = phi|X() as Element of Funcs(A() /\ X(), B() /\ Y()) by A16,FUNCT_2:def 2;
phi|X() in Funcs(A() /\ X(), B() /\ Y()) by A17,A16,FUNCT_2:def 2;
then
A18: x in dom F by FUNCT_2:def 1;
y = F.x by A13,A14;
hence thesis by A18,FUNCT_1:def 6;
end;
hence contradiction by A1,A2,A5;
end;
:: Schematy zwiazane z pewnikiem wyboru
scheme
FunctChoice { A()->non empty set, B()->non empty set, P[(Element of A()),
Element of B()], x()->Element of Fin A() }: ex ff being Function of A(), B() st
for t being Element of A() st t in x() holds P[t,ff.t]
provided
A1: for t being Element of A() st t in x() ex ff being Element of B() st
P[t,ff]
proof
set b = the Element of B();
set M = { { ff where ff is Element of B() : P[tt,ff] } where tt is Element
of A() : tt in x() };
set f = the Function of A(), B();
assume
A2: not thesis;
then consider t being Element of A() such that
A3: t in x() and
not P[t,f.t];
{ ff where ff is Element of B() : P[t,ff] } in M by A3;
then reconsider M as non empty set;
now
let X;
assume X in M;
then consider t being Element of A() such that
A4: X = { ff where ff is Element of B() : P[t,ff] } and
A5: t in x();
consider ff being Element of B() such that
A6: P[t,ff] by A1,A5;
ff in X by A4,A6;
hence X <> {};
end;
then consider Choice being Function such that
dom Choice = M and
A7: X in M implies Choice.X in X by FUNCT_1:111;
defpred Q[(Element of A()),set] means ($1 in x() implies $2 = Choice.{ ff
where ff is Element of B() : P[$1,ff] }) & ($1 in x() or $2 = b);
A8: now
let t be Element of A();
A9: now
set s = { ff where ff is Element of B() : P[t,ff] };
assume t in x();
then s in M;
then Choice.s in s by A7;
then ex ff being Element of B() st Choice.s = ff & P[t,ff];
hence Choice.s is Element of B();
end;
t in x() implies t in x();
hence ex y being Element of B() st Q[t,y] by A9;
end;
consider f being Function of A(), B() such that
A10: for x being Element of A() holds Q[x,f.x] from FUNCT_2:sch 3(A8);
now
let t be Element of A();
assume
A11: t in x();
then
A12: { ff where ff is Element of B() : P[t,ff] } in M;
f.t = Choice.{ ff where ff is Element of B() : P[t,ff] } by A10,A11;
then f.t in { ff where ff is Element of B() : P[t,ff] } by A7,A12;
then ex ff being Element of B() st f.t = ff & P[t,ff];
hence P[t,f.t];
end;
hence contradiction by A2;
end;
scheme
FuncsChoice { A()->non empty set, B()->non empty set, P[Element of A(),
Element of B()], x()->Element of Fin A() }: ex ff being Element of Funcs(A(),B(
)) st for t being Element of A() st t in x() holds P[t,ff.t]
provided
A1: for t being Element of A() st t in x() ex ff being Element of B() st
P[t,ff]
proof
A2: for t being Element of A() st t in x() ex ff being Element of B() st P[t
,ff] by A1;
consider ff being Function of A(), B() such that
A3: for t being Element of A() st t in x() holds P[t,ff.t] from
FunctChoice(A2);
reconsider ff as Element of Funcs(A(),B()) by FUNCT_2:8;
take ff;
thus thesis by A3;
end;
scheme
FraenkelFin9 { A,B() -> non empty set, X() -> set, P[object,object] }:
{ x where x
is Element of B(): ex w being Element of A() st P[w,x] & w in X() } is finite
provided
A1: X() is finite and
A2: for w being Element of A(), x,y being Element of B() st P[w,x] & P[w
,y] holds x = y
proof
set M = { x where x is Element of B(): ex w being Element of A() st P[w,x] &
w in X() };
defpred Q[object,object] means P[$1,$2] & $1 in X() & $2 in B();
A3: for x,y being object st x in A() & Q[x,y] holds y in B();
A4: for x,y1,y2 being object st x in A() & Q[x,y1] & Q[x,y2] holds y1 = y2
by A2;
consider f being PartFunc of A(),B() such that
A5: for x being object holds x in dom f iff x in A() &
ex y being object st Q[x,y] and
A6: for x being object st x in dom f holds Q[x,f.x]
from PARTFUN1:sch 2(A3,A4);
M = f.:X()
proof
thus M c= f.:X()
proof
let x be object;
assume x in M;
then consider u being Element of B() such that
A7: x = u and
A8: ex w being Element of A() st P[w,u] & w in X();
consider w being Element of A() such that
A9: P[w,u] and
A10: w in X() by A8;
A11: w in dom f by A5,A9,A10;
then Q[w,f.w] by A6;
then f.w = x by A2,A7,A9;
hence thesis by A10,A11,FUNCT_1:def 6;
end;
let x be object;
assume x in f.:X();
then consider y being object such that
A12: y in dom f and
A13: y in X() and
A14: x = f.y by FUNCT_1:def 6;
reconsider x as Element of B() by A6,A12,A14;
P[y,x] by A6,A12,A14;
hence thesis by A12,A13;
end;
hence thesis by A1;
end;