The abstract of the Mizar article:

Function Domains and Fr\aenkel Operator

by

Andrzej Trybulec

Received February 7, 1990

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