:: FRAENKEL semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FRAENKEL:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: FRAENKEL:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: FRAENKEL:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set holds Funcs A,B c= bool [:A,B:]
proof end;

theorem Th6: :: FRAENKEL:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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

:: deftheorem Def1 defines functional FRAENKEL:def 1 :
for IT being set holds
( IT is functional iff for x being set st x in IT holds
x is Function );

registration
cluster non empty functional set ;
existence
ex b1 being set st
( not b1 is empty & b1 is functional )
proof end;
end;

registration
let P be functional set ;
cluster -> Relation-like Function-like Element of P;
coherence
for b1 being Element of P holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

theorem :: FRAENKEL:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: FRAENKEL:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function holds {f} is functional
proof end;

registration
let A, B be set ;
cluster Funcs A,B -> functional ;
coherence
Funcs A,B is functional
proof end;
end;

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

:: deftheorem Def2 defines FUNCTION_DOMAIN FRAENKEL:def 2 :
for A, B being set
for b3 being non empty functional set holds
( b3 is FUNCTION_DOMAIN of A,B iff for x being Element of b3 holds x is Function of A,B );

theorem :: FRAENKEL:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FRAENKEL:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, C being set
for f being Function of A,C holds {f} is FUNCTION_DOMAIN of A,C
proof end;

theorem Th11: :: FRAENKEL:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being non empty set
for A being set holds Funcs A,B is FUNCTION_DOMAIN of A,B
proof end;

definition
let A be set ;
let B be non empty set ;
:: original: Funcs
redefine func Funcs A,B -> FUNCTION_DOMAIN of A,B;
coherence
Funcs A,B is FUNCTION_DOMAIN of A,B by Th11;
let F be FUNCTION_DOMAIN of A,B;
:: original: Element
redefine mode Element of F -> Function of A,B;
coherence
for b1 being Element of F holds b1 is Function of A,B by Def2;
end;

theorem :: FRAENKEL:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FRAENKEL:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th14: :: FRAENKEL:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being non empty set
for A, X 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 functional ;
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;

theorem :: FRAENKEL:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being functional set
for B being set st B c= F holds
B is functional
proof end;