:: 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
Fraenkel5'{ F1() -> non empty 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]
proof end;

scheme :: FRAENKEL:sch 2
Fraenkel5''{ F1() -> non empty set , F2() -> non empty 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
Fraenkel6'{ F1() -> non empty 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
Fraenkel6''{ F1() -> non empty set , F2() -> non empty 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
FraenkelF'{ F1() -> non empty 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
FraenkelF'R{ F1() -> non empty 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
FraenkelF''{ F1() -> non empty set , F2() -> non empty 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
FraenkelF6''{ F1() -> non empty set , F2() -> non empty 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 non empty 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() -> non empty set , F2() -> non empty set , F3() -> set , F4() -> Function of F1(),F2(), F5() -> Function of F1(),F2(), P1[ set ], P2[ set ] } :
{ (F4() . u') where u' is Element of F1() : ( P1[u'] & u' in F3() ) } = { (F5() . v') where v' is Element of F1() : ( P2[v'] & v' 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
Gen1''{ F1() -> non empty set , F2() -> non empty 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
Gen1''A{ F1() -> non empty set , F2() -> non empty 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
Gen2''{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty 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
Gen3'{ F1() -> non empty 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
Gen3''{ F1() -> non empty set , F2() -> non empty 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
Gen4''{ F1() -> non empty set , F2() -> non empty 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 s' being Element of F1() st
( P2[s',t] & F3(s,t) = F3(s',t) )
proof end;

scheme :: FRAENKEL:sch 17
FrSet1{ F1() -> non empty 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() -> non empty 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() -> non empty set , F2() -> non empty 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(s',F4()) where s' is Element of F1() : P1[s',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() -> non empty set , F2() -> non empty 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(s',F4()) where s' is Element of F1() : P1[s',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(u',v') where u' is Element of F1(), v' is Element of F2() : ( u' in F3() & v' 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 t' being Element of F2() st
( t' in F3() & t = F4(t') & P1[t,t'] ) )
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() -> non empty set , F2() -> non empty set , F3() -> set , F4() -> set , F5( set ) -> set } :
{ F5(phi') where phi' is Element of Funcs F1(),F2() : phi' .: 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
FraenkelFin'{ 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;