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


begin

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

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

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] )
proof end;

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] )
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

theorem :: FRAENKEL:1
canceled;

theorem :: FRAENKEL:2
canceled;

theorem Th3: :: FRAENKEL:3
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
proof end;

theorem :: FRAENKEL:4
canceled;

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

theorem Th6: :: FRAENKEL:6
for B being non empty set
for A, X, Y being set st Funcs (X,Y) <> {} & X c= A & Y c= B holds
for f being Element of Funcs (X,Y) holds f is PartFunc of A,B
proof end;

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] & u9 in F3() ) } = { (F5() . v9) where v9 is Element of F1() : ( P2[v9] & 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] )
proof end;

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

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

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)]
proof end;

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] } & P2[st1] ) } = { F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] ) }
proof end;

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] } & P1[s] ) } = { F2(s2) where s2 is Element of F1() : ( P2[s2] & P1[s2] ) }
proof end;

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] } & P1[s,t] ) } = { F3(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P2[s2] & P1[s2,t2] ) }
proof end;

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] & F3(s,t) = F3(s9,t) )
proof end;

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() & P1[y] ) } c= F2()
proof end;

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

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() & P1[s,t] ) )
proof end;

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() & P1[s,t] ) } = { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] }
proof end;

theorem :: FRAENKEL:7
canceled;

theorem :: FRAENKEL:8
canceled;

theorem :: FRAENKEL:9
canceled;

theorem :: FRAENKEL:10
canceled;

theorem :: FRAENKEL:11
canceled;

theorem :: FRAENKEL:12
canceled;

theorem :: FRAENKEL:13
canceled;

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

theorem Th15: :: FRAENKEL:15
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)
proof end;

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

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

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() & P1[y,x] & ( for z being Element of F1() st z in F2() & 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] & P1[y,z] holds
P1[x,z]
proof end;

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() & t = F4(t9) & P1[t,t9] ) )
proof end;

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

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

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)
proof end;

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

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

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] & 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] & P1[w,y] holds
x = y
proof end;