Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Function Domains and Fr\aenkel Operator

by
Andrzej Trybulec

MML identifier: FRAENKEL
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, FUNCT_2, BOOLE, PARTFUN1, FINSET_1, MCART_1,
FINSUB_1, SETWISEO, FRAENKEL;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FINSET_1,
FINSUB_1, FUNCT_1, FUNCT_2, DOMAIN_1, PARTFUN1, SETWISEO;
constructors FINSET_1, DOMAIN_1, SETWISEO, XBOOLE_0;
clusters FINSUB_1, FUNCT_1, RELSET_1, SUBSET_1, FINSET_1, RELAT_1, ZFMISC_1,
XBOOLE_0;
requirements BOOLE, SUBSET;

begin

reserve B for non empty set,
A,C,X,x for set;

scheme Fraenkel5'{ A() -> non empty set, F(set) -> set, P[set], Q[set] } :
{ F(v') where v' is Element of A() : P[v'] }
c= { F(u') where u' is Element of A() : Q[u'] }
provided  for v being Element of A() holds P[v] implies Q[v];

scheme Fraenkel5''
{ A() -> non empty set, B() -> non empty set
, F(set,set) -> set, P[set,set], Q[set,set] } :
{ 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
for u being (Element of A()), v being Element of B()
holds P[u,v] implies Q[u,v];

scheme Fraenkel6'{ B() -> non empty set, F(set) -> set, P[set], Q[set] } :
{ F(v1) where v1 is Element of B() : P[v1] }
= { F(v2) where v2 is Element of B() : Q[v2] }
provided
for v being Element of B() holds P[v] iff Q[v];

scheme Fraenkel6''
{ A() -> non empty set, B() -> non empty set
, F(set,set) -> set, P[set,set], Q[set,set] } :
{ 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
for u being (Element of A()), v being Element of B()
holds P[u,v] iff Q[u,v];

scheme FraenkelF'{ B() -> non empty set
, F(set) -> set, G(set) -> set, P[set] } :
{ F(v1) where v1 is Element of B() : P[v1] }
= { G(v2) where v2 is Element of B() : P[v2] }
provided
for v being Element of B() holds F(v) = G(v);

scheme FraenkelF'R{ B() -> non empty set
, F(set) -> set, G(set) -> set, P[set] } :
{ F(v1) where v1 is Element of B() : P[v1] }
= { G(v2) where v2 is Element of B() : P[v2] }
provided
for v being Element of B() st P[v] holds F(v) = G(v);

scheme FraenkelF''
{ A() -> non empty set, B() -> non empty set,
F(set,set) -> set, G(set,set) -> set, P[set,set] } :
{ 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
for u being (Element of A()), v being Element of B()
holds F(u,v) = G(u,v);

scheme FraenkelF6''
{ A() -> non empty set, B() -> non empty set
, F(set,set) -> set, P[set,set], Q[set,set] } :
{ 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
for u being (Element of A()), v being Element of B()
holds P[u,v] iff Q[u,v]
and
for u being (Element of A()), v being Element of B()
holds F(u,v) = F(v,u);

canceled 2;

theorem :: FRAENKEL:3
for A,B being non empty 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;

canceled;

theorem :: FRAENKEL:5
for A,B being set holds Funcs(A,B) c= bool [:A,B:];

theorem :: FRAENKEL:6
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;

scheme RelevantArgs
{ A() -> non empty set, B() -> non empty set, X() -> set,
f() -> (Function of A(),B()), g() -> (Function of A(),B()),
P[set], Q[set] } :
{ f().u' where u' is Element of A() : P[u'] & u' in X() }
= { g().v' where v' is Element of A() : Q[v'] & v' in X() }
provided
f()|X() = g()|X() and
for u being Element of A() st u in X() holds P[u] iff Q[u];

scheme Fr_Set0{ A() -> non empty set, P[set] }:
{ x where x is Element of A(): P[x] } c= A();

scheme Gen1''{A() -> non empty set, B() -> non empty set, F(set,set) -> set,
P[set, set], Q[set] } :
for s being (Element of A()), t being Element of B()
st P[s,t] holds Q[F(s,t)]
provided
for s_t being set st s_t in
{ F(s1,t1) where s1 is (Element of A()), t1 is Element of B(): P[s1,t1] }
holds Q[s_t];

scheme Gen1''A{A() -> non empty set, B() -> non empty set, F(set,set) -> set,
P[set, set], Q[set] } :
for s_t being set st s_t in
{ F(s1,t1) where s1 is (Element of A()), t1 is Element of B(): P[s1,t1] }
holds Q[s_t]
provided
for s being (Element of A()), t being Element of B()
st P[s,t] holds Q[F(s,t)];

scheme Gen2''{A() -> non empty set, B() -> non empty set, C() -> non empty set,
F(set,set) -> (Element of C()),
P[set, set], Q[set] } :
{ s_t where s_t is Element of C()
: s_t in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B()
: P[s1,t1] }
& Q[s_t] }
= { F(s2,t2) where s2 is (Element of A()), t2 is Element of B()
: P[s2,t2] & Q[F(s2,t2)]};

scheme Gen3'{A() -> non empty set, F(set) -> set, P[set], Q[set] } :
{ 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] };

scheme Gen3''{A() -> non empty set, B() -> non empty set, F(set,set) -> set,
P[set, set], Q[set] } :
{ 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] };

scheme Gen4''{A() -> non empty set, B() -> non empty set, F(set,set) -> set,
P[set, set], Q[set,set] } :
{ 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
for s being (Element of A()), t being Element of B() st P[s,t]
ex s' being Element of A() st Q[s',t] & F(s,t) = F(s',t);

scheme FrSet_1{ D() -> non empty set, A() -> set, P[set], F(set) -> set }:
{ F(y) where y is Element of D() : F(y) in A() & P[y] } c= A();

scheme FrSet_2{ D() -> non empty set, A() -> set, Q[set], F(set) -> set }:
{ F(y) where y is Element of D() : Q[y] & not F(y) in A() } misses A();

scheme FrEqua1{ A()-> non empty set, B() -> non empty set, F(set,set) -> set,
x() -> (Element of B()), P[set,set], Q[set,set] }:
{ F(s,t) where s is (Element of A()), t is Element of B(): Q[s,t] }
= { F(s',x()) where s' is Element of A(): P[s',x()] }
provided
for s being Element of A() for t being Element of B() holds
Q[s,t] iff t = x() & P[s,t];

scheme FrEqua2{ A()-> non empty set, B() -> non empty set, F(set,set) -> set,
x() -> (Element of B()), P[set,set] }:
{ F(s,t) where s is (Element of A()), t is Element of B(): t = x() & P[s,t] }
= { F(s',x()) where s' is Element of A(): P[s',x()] };

:: dziedziny funkcji

definition let IT be set;
attr IT is functional means
:: FRAENKEL:def 1
for x being set st x in IT holds x is Function;
end;

definition
cluster non empty functional set;
end;

definition let P be functional set;
cluster -> Function-like Relation-like Element of P;
end;

canceled;

theorem :: FRAENKEL:8
for f being Function holds { f } is functional;

definition let A, B be set;
cluster Funcs(A,B) -> functional;
end;

definition let A, B be set;
mode FUNCTION_DOMAIN of A,B -> functional non empty set means
:: FRAENKEL:def 2
for x being Element of it holds x is Function of A,B;
end;

canceled;

theorem :: FRAENKEL:10
for f being Function of A,C holds { f } is FUNCTION_DOMAIN of A,C;

theorem :: FRAENKEL:11
Funcs(A,B) is FUNCTION_DOMAIN of A,B;

definition let A be set, B be non empty set;
redefine func Funcs(A,B) -> FUNCTION_DOMAIN of A,B;
let F be FUNCTION_DOMAIN of A,B;
mode Element of F -> Function of A,B;
end;

reserve phi for Element of Funcs(A,B);

canceled 2;

theorem :: FRAENKEL:14
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;

theorem :: FRAENKEL:15
for X being set, phi holds phi|X = phi|(A /\ X);

:: Zbiory skonczone

scheme FraenkelFin { A() ->non empty set, X() -> set, F(set) -> set }:
{ F(w) where w is Element of A(): w in X() } is finite
provided
X() is finite;

scheme CartFin { A, B() -> non empty set, X, Y() -> set, F(set, set) -> set }:
{ F(u',v') where u' is (Element of A()), v' is Element of B()
: u' in X() & v' in Y() } is finite
provided
X() is finite and
Y() is finite;

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
for x being Element of A() holds P[x,x] and
for x,y,z being Element of A() st P[x,y] & P[y,z] holds P[x,z];

scheme Fin_Im{A() ->non empty set, B()->non empty set
, x()-> (Element of Fin B()),
F(set)->(Element of A()), P[set,set]}:
ex c1 being Element of Fin A() st
for t being Element of A() holds t in c1 iff
ex t' being Element of B() st t' in x() & t = F(t') & P[t,t'];

theorem :: FRAENKEL:16
for A,B being set st A is finite & B is finite holds
Funcs(A,B) is finite;

scheme ImFin { A() -> non empty set, B() -> non empty set,
X() -> set, Y() -> set, F(set) -> set } :
{ F(phi') where phi' is Element of Funcs(A(),B()):
phi'.:X() c= Y() } is finite
provided
X() is finite and
Y() is finite and
for phi,psi being Element of Funcs(A(),B())
holds phi|X() = psi|X() implies F(phi) = F(psi);

:: 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
for t being Element of A() st t in x()
ex ff being Element of B() st P[t,ff];

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
for t being Element of A() st t in x()
ex ff being Element of B() st P[t,ff];
```