:: Function Domains and Fr{\ae}nkel Operator
:: by Andrzej Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

scheme :: FRAENKEL:sch 1
Fraenkel59{ F1() ->  set , F2( set ) ->  set , P1[ set ], P2[ set ] } :
  {  F2(v) where v is Element of F1() : P1[v]  }  c=  {  F2(u) where u is Element of F1() : P2[u]  }
provided
A1: for v being Element of F1() st P1[v] holds
P2[v]
proofend;

scheme :: FRAENKEL:sch 2
Fraenkel599{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set , set ] } :
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  c=  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }
provided
A1: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
P2[u,v]
proofend;

scheme :: FRAENKEL:sch 3
Fraenkel69{ F1() ->  set , F2( set ) ->  set , P1[ set ], P2[ set ] } :
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F2(v2) where v2 is Element of F1() : P2[v2]  }
provided
A1: for v being Element of F1() holds
( P1[v] iff P2[v] )
proofend;

scheme :: FRAENKEL:sch 4
Fraenkel699{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set , set ] } :
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }
provided
A1: for u being Element of F1()
for v being Element of F2() holds
( P1[u,v] iff P2[u,v] )
proofend;

scheme :: FRAENKEL:sch 5
FraenkelF9{ F1() ->  set , F2( set ) ->  set , F3( set ) ->  set , P1[ set ] } :
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
provided
A1: for v being Element of F1() holds F2(v) = F3(v)
proofend;

scheme :: FRAENKEL:sch 6
FraenkelF9R{ F1() ->  set , F2( set ) ->  set , F3( set ) ->  set , P1[ set ] } :
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proofend;

scheme :: FRAENKEL:sch 7
FraenkelF99{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }
provided
A1: for u being Element of F1()
for v being Element of F2() holds F3(u,v) = F4(u,v)
proofend;

scheme :: FRAENKEL:sch 8
FraenkelF699{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set , set ] } :
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F3(v2,u2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }
provided
A1: for u being Element of F1()
for v being Element of F2() holds
( P1[u,v] iff P2[u,v] ) and
A2: for u being Element of F1()
for v being Element of F2() holds F3(u,v) = F3(v,u)
proofend;

theorem Th1: :: FRAENKEL:1
for A, B being set
for F, G being Function of A,B
for X being set st F | X = G | X holds
for x being Element of A st x in X holds
F . x = G . x
proofend;

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

theorem Th3: :: FRAENKEL:3
for B being non empty set
for A, X, Y being set st Funcs (X,Y) <> {} &amp; X c= A &amp; Y c= B holds
for f being Element of Funcs (X,Y) holds f is PartFunc of A,B
proofend;

scheme :: FRAENKEL:sch 9
RelevantArgs{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  Function of F1(),F2(), F5() ->  Function of F1(),F2(), P1[ set ], P2[ set ] } :
  {  (F4() . u9) where u9 is Element of F1() : ( P1[u9] &amp; u9 in F3() )  }  =  {  (F5() . v9) where v9 is Element of F1() : ( P2[v9] &amp; v9 in F3() )  }
provided
A1: F4() | F3() = F5() | F3() and
A2: for u being Element of F1() st u in F3() holds
( P1[u] iff P2[u] )
proofend;

scheme :: FRAENKEL:sch 10
FrSet0{ F1() ->  non empty set , P1[ set ] } :
  {  x where x is Element of F1() : P1[x]  }  c= F1()
proofend;

scheme :: FRAENKEL:sch 11
Gen199{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set ] } :
 for s being Element of F1()
for t being Element of F2() st P1[s,t] holds
P2[F3(s,t)]
provided
A1: for st1 being set st st1 in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  holds
P2[st1]
proofend;

scheme :: FRAENKEL:sch 12
Gen199A{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set ] } :
 for st1 being set st st1 in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  holds
P2[st1]
provided
A1: for s being Element of F1()
for t being Element of F2() st P1[s,t] holds
P2[F3(s,t)]
proofend;

scheme :: FRAENKEL:sch 13
Gen299{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  Element of F3(), P1[ set , set ], P2[ set ] } :
  {  st1 where st1 is Element of F3() : ( st1 in  {  F4(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  &amp; P2[st1] )  }  =  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] &amp; P2[F4(s2,t2)] )  }
proofend;

scheme :: FRAENKEL:sch 14
Gen39{ F1() ->  set , F2( set ) ->  set , P1[ set ], P2[ set ] } :
  {  F2(s) where s is Element of F1() : ( s in  {  s1 where s1 is Element of F1() : P2[s1]  }  &amp; P1[s] )  }  =  {  F2(s2) where s2 is Element of F1() : ( P2[s2] &amp; P1[s2] )  }
proofend;

scheme :: FRAENKEL:sch 15
Gen399{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set ] } :
  {  F3(s,t) where s is Element of F1(), t is Element of F2() : ( s in  {  s1 where s1 is Element of F1() : P2[s1]  }  &amp; P1[s,t] )  }  =  {  F3(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P2[s2] &amp; P1[s2,t2] )  }
proofend;

scheme :: FRAENKEL:sch 16
Gen499{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , P1[ set , set ], P2[ set , set ] } :
  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P1[s,t]  }  c=  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P2[s1,t1]  }
provided
A1: for s being Element of F1()
for t being Element of F2() st P1[s,t] holds
ex s9 being Element of F1() st
( P2[s9,t] &amp; F3(s,t) = F3(s9,t) )
proofend;

scheme :: FRAENKEL:sch 17
FrSet1{ F1() ->  set , F2() ->  set , P1[ set ], F3( set ) ->  set } :
  {  F3(y) where y is Element of F1() : ( F3(y) in F2() &amp; P1[y] )  }  c= F2()
proofend;

scheme :: FRAENKEL:sch 18
FrSet2{ F1() ->  set , F2() ->  set , P1[ set ], F3( set ) ->  set } :
  {  F3(y) where y is Element of F1() : ( P1[y] &amp; not F3(y) in F2() )  }  misses F2()
proofend;

scheme :: FRAENKEL:sch 19
FrEqua1{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , F4() ->  Element of F2(), P1[ set , set ], P2[ set , set ] } :
  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }  =  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }
provided
A1: for s being Element of F1()
for t being Element of F2() holds
( P2[s,t] iff ( t = F4() &amp; P1[s,t] ) )
proofend;

scheme :: FRAENKEL:sch 20
FrEqua2{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set , F4() ->  Element of F2(), P1[ set , set ] } :
  {  F3(s,t) where s is Element of F1(), t is Element of F2() : ( t = F4() &amp; P1[s,t] )  }  =  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }
proofend;

theorem Th4: :: FRAENKEL:4
for B being non empty set
for A, X, Y being set st Funcs (X,Y) <> {} &amp; X c= A &amp; Y c= B holds
for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f
proofend;

theorem Th5: :: FRAENKEL:5
for B being non empty set
for X, A being set
for phi being Element of Funcs (A,B) holds phi | X = phi | (A /\ X)
proofend;

scheme :: FRAENKEL:sch 21
FraenkelFin{ F1() ->  set , F2() ->  set , F3( set ) ->  set } :
  {  F3(w) where w is Element of F1() : w in F2()  }  is finite
provided
A1: F2() is finite
proofend;

scheme :: FRAENKEL:sch 22
CartFin{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  set , F4() ->  set , F5( set , set ) ->  set } :
  {  F5(u,v) where u is Element of F1(), v is Element of F2() : ( u in F3() &amp; v in F4() )  }  is finite
provided
A1: F3() is finite and
A2: F4() is finite
proofend;

scheme :: FRAENKEL:sch 23
Finiteness{ F1() ->  non empty set , F2() ->  Element of Fin F1(), P1[ Element of F1(), Element of F1()] } :
 for x being Element of F1() st x in F2() holds
ex y being Element of F1() st
( y in F2() &amp; P1[y,x] &amp; ( for z being Element of F1() st z in F2() &amp; P1[z,y] holds
P1[y,z] ) )
provided
A1: for x being Element of F1() holds P1[x,x] and
A2: for x, y, z being Element of F1() st P1[x,y] &amp; P1[y,z] holds
P1[x,z]
proofend;

scheme :: FRAENKEL:sch 24
FinIm{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  Element of Fin F2(), F4( set ) ->  Element of F1(), P1[ set , set ] } :
 ex c1 being Element of Fin F1() st
for t being Element of F1() holds
( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() &amp; t = F4(t9) &amp; P1[t,t9] ) )
proofend;

registration
let A, B be finite set ;
cluster Funcs (A,B) ->  finite ;
coherence
 Funcs (A,B) is finite
proofend;
end;

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

scheme :: FRAENKEL:sch 25
ImFin{ F1() ->  set , F2() ->  non empty set , F3() ->  set , F4() ->  set , F5( set ) ->  set } :
  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  is finite
provided
A1: F3() is finite and
A2: F4() is finite and
A3: for phi, psi being Element of Funcs (F1(),F2()) st phi | F3() = psi | F3() holds
F5(phi) = F5(psi)
proofend;

scheme :: FRAENKEL:sch 26
FunctChoice{ F1() ->  non empty set , F2() ->  non empty set , P1[ Element of F1(), Element of F2()], F3() ->  Element of Fin F1() } :
 ex ff being Function of F1(),F2() st
for t being Element of F1() st t in F3() holds
P1[t,ff . t]
provided
A1: for t being Element of F1() st t in F3() holds
ex ff being Element of F2() st P1[t,ff]
proofend;

scheme :: FRAENKEL:sch 27
FuncsChoice{ F1() ->  non empty set , F2() ->  non empty set , P1[ Element of F1(), Element of F2()], F3() ->  Element of Fin F1() } :
 ex ff being Element of Funcs (F1(),F2()) st
for t being Element of F1() st t in F3() holds
P1[t,ff . t]
provided
A1: for t being Element of F1() st t in F3() holds
ex ff being Element of F2() st P1[t,ff]
proofend;

scheme :: FRAENKEL:sch 28
FraenkelFin9{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  set , P1[ set , set ] } :
  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] &amp; w in F3() )  }  is finite
provided
A1: F3() is finite and
A2: for w being Element of F1()
for x, y being Element of F2() st P1[w,x] &amp; P1[w,y] holds
x = y
proofend;