:: FRAENKEL semantic presentation

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]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F2(v) where v is Element of F1() : P1[v]  }  or x in  {  F2(u) where u is Element of F1() : P2[u]  }  )
assume  x in  {  F2(v9) where v9 is Element of F1() : P1[v9]  }  ; ::_thesis: x in  {  F2(u) where u is Element of F1() : P2[u]  }
then consider v being Element of F1() such that
A2: x = F2(v) and
A3: P1[v] ;
 P2[v] by A1, A3;
hence  x in  {  F2(u) where u is Element of F1() : P2[u]  }  by A2; ::_thesis: verum
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
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  or x in  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  )
assume  x in  {  F3(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : P1[u9,v9]  }  ; ::_thesis: x in  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }
then consider u being Element of F1(), v being Element of F2() such that
A2: x = F3(u,v) and
A3: P1[u,v] ;
 P2[u,v] by A1, A3;
hence  x in  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  by A2; ::_thesis: verum
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
set A =  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ;
set B =  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  ;
A2: for v being Element of F1() st P1[v] holds
P2[v] by A1;
thus   {  F2(v1) where v1 is Element of F1() : P1[v1]  }  c=  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  from FRAENKEL:sch_1(A2); :: according to XBOOLE_0:def_10 ::_thesis:  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
A3: for v being Element of F1() st P2[v] holds
P1[v] by A1;
thus   {  F2(v2) where v2 is Element of F1() : P2[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  from FRAENKEL:sch_1(A3); ::_thesis: verum
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
set B =  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  ;
set A =  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  ;
A2: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
P2[u,v] by A1;
thus   {  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]  }  from FRAENKEL:sch_2(A2); :: according to XBOOLE_0:def_10 ::_thesis:  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  c=  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }
A3: for u being Element of F1()
for v being Element of F2() st P2[u,v] holds
P1[u,v] by A1;
thus   {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  c=  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  from FRAENKEL:sch_2(A3); ::_thesis: verum
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
set X =  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ;
set Y =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ;
A2:  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  or x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  )
assume  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ; ::_thesis: x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
 x = F2(v1) by A1, A3;
hence  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  by A4; ::_thesis: verum
end;
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  c=  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  or x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  )
assume  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ; ::_thesis: x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
 x = F3(v1) by A1, A5;
hence  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A6; ::_thesis: verum
end;
hence   {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
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
set X =  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ;
set Y =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ;
A2:  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  or x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  )
assume  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ; ::_thesis: x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
 x = F2(v1) by A1, A3, A4;
hence  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  by A4; ::_thesis: verum
end;
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  c=  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  or x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  )
assume  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ; ::_thesis: x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
 x = F3(v1) by A1, A5, A6;
hence  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A6; ::_thesis: verum
end;
hence   {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
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
set Y =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  ;
set X =  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  ;
A2:  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  c=  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  or x in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  )
assume  x in  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  ; ::_thesis: x in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }
then consider u1 being Element of F1(), v1 being Element of F2() such that
A3: x = F4(u1,v1) and
A4: P1[u1,v1] ;
 x = F3(u1,v1) by A1, A3;
hence  x in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  by A4; ::_thesis: verum
end;
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  c=  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  or x in  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  )
assume  x in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  ; ::_thesis: x in  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }
then consider u1 being Element of F1(), v1 being Element of F2() such that
A5: x = F3(u1,v1) and
A6: P1[u1,v1] ;
 x = F4(u1,v1) by A1, A5;
hence  x in  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  by A6; ::_thesis: verum
end;
hence   {  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]  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
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
A3: for u being Element of F1()
for v being Element of F2() st P2[u,v] holds
P1[u,v] by A1;
A4:  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P2[u1,v1]  }  c=  {  F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  from FRAENKEL:sch_2(A3);
deffunc H1( set , set ) ->  set = F3($2,$1);
A5: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
P2[u,v] by A1;
A6:  {  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]  }  from FRAENKEL:sch_2(A5);
A7: for u being Element of F1()
for v being Element of F2() holds F3(u,v) = H1(u,v) by A2;
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P2[u1,v1]  }  =  {  H1(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  from FRAENKEL:sch_7(A7);
hence   {  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]  }  by A6, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

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
proof
let A, B be set ; ::_thesis: 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
let F, G be Function of A,B; ::_thesis: 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
let X be set ; ::_thesis: ( F | X = G | X implies for x being Element of A st x in X holds
F . x = G . x )
assume A1: F | X = G | X ; ::_thesis: for x being Element of A st x in X holds
F . x = G . x
let x be Element of A; ::_thesis: ( x in X implies F . x = G . x )
assume A2: x in X ; ::_thesis: F . x = G . x
hence F . x = (G | X) . x by A1, FUNCT_1:49
.= G . x by A2, FUNCT_1:49 ;
::_thesis: verum
end;

theorem Th2: :: FRAENKEL:2
for A, B being set holds Funcs (A,B) c= bool [:A,B:]
proof
let A, B be set ; ::_thesis: Funcs (A,B) c= bool [:A,B:]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (A,B) or x in bool [:A,B:] )
assume  x in Funcs (A,B) ; ::_thesis: x in bool [:A,B:]
then consider f being Function such that
A1: x = f and
A2: dom f = A and
A3: rng f c= B by FUNCT_2:def_2;
A4: f c= [:(dom f),(rng f):] by RELAT_1:7;
 [:(dom f),(rng f):] c= [:A,B:] by A2, A3, ZFMISC_1:95;
then  f c= [:A,B:] by A4, XBOOLE_1:1;
hence  x in bool [:A,B:] by A1; ::_thesis: verum
end;

theorem Th3: :: FRAENKEL:3
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
let B be non empty set ; ::_thesis: 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
let A be set ; ::_thesis: for 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
let X, Y be set ; ::_thesis: ( Funcs (X,Y) <> {} & X c= A & Y c= B implies for f being Element of Funcs (X,Y) holds f is PartFunc of A,B )
assume that
A1: Funcs (X,Y) <> {} and
A2: X c= A and
A3: Y c= B ; ::_thesis: for f being Element of Funcs (X,Y) holds f is PartFunc of A,B
let f be Element of Funcs (X,Y); ::_thesis: f is PartFunc of A,B
consider g being Function such that
A4: f = g and
A5: dom g = X and
A6: rng g c= Y by A1, FUNCT_2:def_2;
 rng g c= B by A3, A6, XBOOLE_1:1;
hence  f is PartFunc of A,B by A2, A4, A5, RELSET_1:4; ::_thesis: verum
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
deffunc H1( set ) ->  set = F4() . $1;
deffunc H2( set ) ->  set = F5() . $1;
defpred S1[ set ] means ( P1[$1] & $1 in F3() );
defpred S2[ set ] means ( P2[$1] & $1 in F3() );
set C =  {  H2(v9) where v9 is Element of F1() : S1[v9]  }  ;
A3: for v being Element of F1() holds
( S1[v] iff S2[v] ) by A2;
A4:  {  H2(v9) where v9 is Element of F1() : S1[v9]  }  =  {  H2(v9) where v9 is Element of F1() : S2[v9]  }  from FRAENKEL:sch_3(A3);
A5: for v being Element of F1() st S1[v] holds
H1(v) = H2(v) by A1, Th1;
  {  H1(u9) where u9 is Element of F1() : S1[u9]  }  =  {  H2(v9) where v9 is Element of F1() : S1[v9]  }  from FRAENKEL:sch_6(A5);
hence   {  (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() )  }  by A4; ::_thesis: verum
end;

scheme :: FRAENKEL:sch 10
FrSet0{ F1() ->  non empty set , P1[ set ] } :
  {  x where x is Element of F1() : P1[x]  }  c= F1()
proof
  {  x where x is Element of F1() : P1[x]  }  is Subset of F1() from DOMAIN_1:sch_7();
hence   {  x where x is Element of F1() : P1[x]  }  c= F1() ; ::_thesis: verum
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
let s be Element of F1(); ::_thesis: for t being Element of F2() st P1[s,t] holds
P2[F3(s,t)]
let t be Element of F2(); ::_thesis: ( P1[s,t] implies P2[F3(s,t)] )
assume  P1[s,t] ; ::_thesis: P2[F3(s,t)]
then  F3(s,t) in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  ;
hence  P2[F3(s,t)] by A1; ::_thesis: verum
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
let st1 be set ; ::_thesis: ( st1 in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  implies P2[st1] )
assume  st1 in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  ; ::_thesis: P2[st1]
then  ex s1 being Element of F1() ex t1 being Element of F2() st
( st1 = F3(s1,t1) & P1[s1,t1] ) ;
hence  P2[st1] by A1; ::_thesis: verum
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
thus   {  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] )  }  c=  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }  c=  {  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] )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  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] )  }  or x in  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }  )
assume  x in  {  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] )  }  ; ::_thesis: x in  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }
then consider st1 being Element of F3() such that
A1: x = st1 and
A2: st1 in  {  F4(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  and
A3: P2[st1] ;
 ex s1 being Element of F1() ex t1 being Element of F2() st
( st1 = F4(s1,t1) & P1[s1,t1] ) by A2;
hence  x in  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }  by A1, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }  or x in  {  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] )  }  )
assume  x in  {  F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] )  }  ; ::_thesis: x in  {  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] )  }
then consider s2 being Element of F1(), t2 being Element of F2() such that
A4: x = F4(s2,t2) and
A5: P1[s2,t2] and
A6: P2[F4(s2,t2)] ;
 F4(s2,t2) in  {  F4(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1]  }  by A5;
hence  x in  {  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] )  }  by A4, A6; ::_thesis: verum
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
defpred S1[ set ] means ( P2[$1] & P1[$1] );
defpred S2[ set ] means ( $1 in  {  s1 where s1 is Element of F1() : P2[s1]  }  & P1[$1] );
A1: for s being Element of F1() holds
( S2[s] iff S1[s] )
proof
let s be Element of F1(); ::_thesis: ( S2[s] iff S1[s] )
now__::_thesis:_(_s_in__{__s1_where_s1_is_Element_of_F1()_:_P2[s1]__}__implies_P2[s]_)
assume  s in  {  s1 where s1 is Element of F1() : P2[s1]  }  ; ::_thesis: P2[s]
then  ex s1 being Element of F1() st
( s = s1 & P2[s1] ) ;
hence  P2[s] ; ::_thesis: verum
end;
hence  ( S2[s] iff S1[s] ) ; ::_thesis: verum
end;
thus   {  F2(s) where s is Element of F1() : S2[s]  }  =  {  F2(s2) where s2 is Element of F1() : S1[s2]  }  from FRAENKEL:sch_3(A1); ::_thesis: verum
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
defpred S1[ set , set ] means ( P2[$1] & P1[$1,$2] );
defpred S2[ set , set ] means ( $1 in  {  s1 where s1 is Element of F1() : P2[s1]  }  & P1[$1,$2] );
A1: for s being Element of F1()
for t being Element of F2() holds
( S2[s,t] iff S1[s,t] )
proof
let s be Element of F1(); ::_thesis: for t being Element of F2() holds
( S2[s,t] iff S1[s,t] )
let t be Element of F2(); ::_thesis: ( S2[s,t] iff S1[s,t] )
now__::_thesis:_(_s_in__{__s1_where_s1_is_Element_of_F1()_:_P2[s1]__}__implies_P2[s]_)
assume  s in  {  s1 where s1 is Element of F1() : P2[s1]  }  ; ::_thesis: P2[s]
then  ex s1 being Element of F1() st
( s = s1 & P2[s1] ) ;
hence  P2[s] ; ::_thesis: verum
end;
hence  ( S2[s,t] iff S1[s,t] ) ; ::_thesis: verum
end;
thus   {  F3(s,t) where s is Element of F1(), t is Element of F2() : S2[s,t]  }  =  {  F3(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : S1[s2,t2]  }  from FRAENKEL:sch_4(A1); ::_thesis: verum
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
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P1[s,t]  }  or x in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P2[s1,t1]  }  )
assume  x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P1[s,t]  }  ; ::_thesis: x in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P2[s1,t1]  }
then consider s being Element of F1(), t being Element of F2() such that
A2: x = F3(s,t) and
A3: P1[s,t] ;
 ex s9 being Element of F1() st
( P2[s9,t] & F3(s,t) = F3(s9,t) ) by A1, A3;
hence  x in  {  F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P2[s1,t1]  }  by A2; ::_thesis: verum
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
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(y) where y is Element of F1() : ( F3(y) in F2() & P1[y] )  }  or x in F2() )
assume  x in  {  F3(y) where y is Element of F1() : ( F3(y) in F2() & P1[y] )  }  ; ::_thesis: x in F2()
then  ex y being Element of F1() st
( x = F3(y) & F3(y) in F2() & P1[y] ) ;
hence  x in F2() ; ::_thesis: verum
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
assume   {  F3(y) where y is Element of F1() : ( P1[y] & not F3(y) in F2() )  }  meets F2() ; ::_thesis: contradiction
then consider x being set  such that
A1: x in  {  F3(y) where y is Element of F1() : ( P1[y] & not F3(y) in F2() )  }  and
A2: x in F2() by XBOOLE_0:3;
 ex y being Element of F1() st
( x = F3(y) & P1[y] & not F3(y) in F2() ) by A1;
hence  contradiction by A2; ::_thesis: verum
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
thus   {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }  c=  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  c=  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }  or x in  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  )
assume  x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }  ; ::_thesis: x in  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }
then consider s being Element of F1(), t being Element of F2() such that
A2: x = F3(s,t) and
A3: P2[s,t] ;
A4: P1[s,t] by A1, A3;
 t = F4() by A1, A3;
hence  x in  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  by A2, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  or x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }  )
assume  x in  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  ; ::_thesis: x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }
then consider s9 being Element of F1() such that
A5: x = F3(s9,F4()) and
A6: P1[s9,F4()] ;
 P2[s9,F4()] by A1, A6;
hence  x in  {  F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t]  }  by A5; ::_thesis: verum
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
defpred S1[ set , set ] means ( $2 = F4() & P1[$1,$2] );
A1: for s being Element of F1()
for t being Element of F2() holds
( S1[s,t] iff ( t = F4() & P1[s,t] ) ) ;
thus   {  F3(s,t) where s is Element of F1(), t is Element of F2() : S1[s,t]  }  =  {  F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()]  }  from FRAENKEL:sch_19(A1); ::_thesis: verum
end;

theorem Th4: :: FRAENKEL:4
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
let B be non empty set ; ::_thesis: 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
let A be set ; ::_thesis: for 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
let X, Y be set ; ::_thesis: ( Funcs (X,Y) <> {} & X c= A & Y c= B implies for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f )
assume that
A1: Funcs (X,Y) <> {} and
A2: X c= A and
A3: Y c= B ; ::_thesis: for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f
let f be Element of Funcs (X,Y); ::_thesis: ex phi being Element of Funcs (A,B) st phi | X = f
reconsider f9 = f as PartFunc of A,B by A1, A2, A3, Th3;
consider phi being Function of A,B such that
A4: for x being set st x in dom f9 holds
phi . x = f9 . x by FUNCT_2:71;
reconsider phi = phi as Element of Funcs (A,B) by FUNCT_2:8;
take  phi ; ::_thesis: phi | X = f
 ex g being Function st
( f = g & dom g = X & rng g c= Y ) by A1, FUNCT_2:def_2;
then  dom f9 = A /\ X by XBOOLE_1:28
.= (dom phi) /\ X by FUNCT_2:def_1 ;
hence  phi | X = f by A4, FUNCT_1:46; ::_thesis: verum
end;

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)
proof
let B be non empty set ; ::_thesis: for X, A being set
for phi being Element of Funcs (A,B) holds phi | X = phi | (A /\ X)
let X, A be set ; ::_thesis: for phi being Element of Funcs (A,B) holds phi | X = phi | (A /\ X)
let phi be Element of Funcs (A,B); ::_thesis: phi | X = phi | (A /\ X)
 dom phi = A by FUNCT_2:def_1;
then A1: dom (phi | X) = ((dom phi) /\ A) /\ X by RELAT_1:61
.= (dom phi) /\ (A /\ X) by XBOOLE_1:16 ;
 for x being set st x in dom (phi | X) holds
(phi | X) . x = phi . x by FUNCT_1:47;
hence  phi | X = phi | (A /\ X) by A1, FUNCT_1:46; ::_thesis: verum
end;

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
proof
set M =  {  F3(w) where w is Element of F1() : w in F2()  }  ;
percases ( F1() is empty or not F1() is empty ) ;
supposeA2: F1() is empty ; ::_thesis:  {  F3(w) where w is Element of F1() : w in F2()  }  is finite
  {  F3(w) where w is Element of F1() : w in F2()  }  c= {F3({})}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(w) where w is Element of F1() : w in F2()  }  or x in {F3({})} )
assume  x in  {  F3(w) where w is Element of F1() : w in F2()  }  ; ::_thesis: x in {F3({})}
then consider w being Element of F1() such that
A3: ( x = F3(w) & w in F2() ) ;
 w = {} by A2, SUBSET_1:def_1;
hence  x in {F3({})} by A3, TARSKI:def_1; ::_thesis: verum
end;
hence   {  F3(w) where w is Element of F1() : w in F2()  }  is finite ; ::_thesis: verum
end;
supposeA4: not F1() is empty ; ::_thesis:  {  F3(w) where w is Element of F1() : w in F2()  }  is finite
consider f being Function such that
A5: dom f = F2() /\ F1() and
A6: for y being set st y in F2() /\ F1() holds
f . y = F3(y) from FUNCT_1:sch_3();
  {  F3(w) where w is Element of F1() : w in F2()  }  = f .: F2()
proof
thus   {  F3(w) where w is Element of F1() : w in F2()  }  c= f .: F2() :: according to XBOOLE_0:def_10 ::_thesis: f .: F2() c=  {  F3(w) where w is Element of F1() : w in F2()  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(w) where w is Element of F1() : w in F2()  }  or x in f .: F2() )
assume  x in  {  F3(w) where w is Element of F1() : w in F2()  }  ; ::_thesis: x in f .: F2()
then consider u being Element of F1() such that
A7: x = F3(u) and
A8: u in F2() ;
A9: u in dom f by A4, A5, A8, XBOOLE_0:def_4;
then  f . u = F3(u) by A5, A6;
hence  x in f .: F2() by A7, A8, A9, FUNCT_1:def_6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: F2() or x in  {  F3(w) where w is Element of F1() : w in F2()  }  )
assume  x in f .: F2() ; ::_thesis: x in  {  F3(w) where w is Element of F1() : w in F2()  }
then consider y being set  such that
A10: y in dom f and
A11: y in F2() and
A12: x = f . y by FUNCT_1:def_6;
reconsider y = y as Element of F1() by A5, A10, XBOOLE_0:def_4;
 x = F3(y) by A5, A6, A10, A12;
hence  x in  {  F3(w) where w is Element of F1() : w in F2()  }  by A11; ::_thesis: verum
end;
hence   {  F3(w) where w is Element of F1() : w in F2()  }  is finite by A1; ::_thesis: verum
end;
end;
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
deffunc H1( set ) ->  set = F5(($1 `1),($1 `2));
set M =  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  ;
consider f being Function such that
A3: dom f = [:(F3() /\ F1()),(F4() /\ F2()):] and
A4: for y being set st y in [:(F3() /\ F1()),(F4() /\ F2()):] holds
f . y = H1(y) from FUNCT_1:sch_3();
A5: dom f = [:F3(),F4():] /\ [:F1(),F2():] by A3, ZFMISC_1:100;
  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  = f .: [:F3(),F4():]
proof
thus   {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  c= f .: [:F3(),F4():] :: according to XBOOLE_0:def_10 ::_thesis: f .: [:F3(),F4():] c=  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  or x in f .: [:F3(),F4():] )
assume  x in  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  ; ::_thesis: x in f .: [:F3(),F4():]
then consider u being Element of F1(), v being Element of F2() such that
A6: x = F5(u,v) and
A7: u in F3() and
A8: v in F4() ;
A9: [u,v] in [:F3(),F4():] by A7, A8, ZFMISC_1:87;
then A10: [u,v] in dom f by A5, XBOOLE_0:def_4;
A11: [u,v] `2 = v ;
 [u,v] `1 = u ;
then  f . (u,v) = F5(u,v) by A3, A4, A10, A11;
hence  x in f .: [:F3(),F4():] by A6, A9, A10, FUNCT_1:def_6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: [:F3(),F4():] or x in  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  )
assume  x in f .: [:F3(),F4():] ; ::_thesis: x in  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }
then consider y being set  such that
A12: y in dom f and
A13: y in [:F3(),F4():] and
A14: x = f . y by FUNCT_1:def_6;
reconsider y = y as Element of [:F1(),F2():] by A5, A12, XBOOLE_0:def_4;
A15: y = [(y `1),(y `2)] by MCART_1:21;
then A16: y `1 in F3() by A13, ZFMISC_1:87;
A17: y `2 in F4() by A13, A15, ZFMISC_1:87;
 x = F5((y `1),(y `2)) by A3, A4, A12, A14;
hence  x in  {  F5(u9,v9) where u9 is Element of F1(), v9 is Element of F2() : ( u9 in F3() & v9 in F4() )  }  by A16, A17; ::_thesis: verum
end;
hence   {  F5(u,v) where u is Element of F1(), v is Element of F2() : ( u in F3() & v in F4() )  }  is finite by A1, A2; ::_thesis: verum
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
defpred S1[ Element of F1(), Element of Fin F1()] means  ex y being Element of F1() st
( y in $2 & P1[y,$1] & ( for z being Element of F1() st z in $2 & P1[z,y] holds
P1[y,z] ) );
defpred S2[ Element of Fin F1()] means  for x being Element of F1() st x in $1 holds
S1[x,$1];
A3: now__::_thesis:_for_B_being_Element_of_Fin_F1()
for_x_being_Element_of_F1()_st_S2[B]_holds_
S2[B_\/_{.x.}]
let B be Element of Fin F1(); ::_thesis: for x being Element of F1() st S2[B] holds
S2[B \/ {.x.}]
let x be Element of F1(); ::_thesis: ( S2[B] implies S2[B \/ {.x.}] )
assume A4: S2[B] ; ::_thesis: S2[B \/ {.x.}]
thus  S2[B \/ {.x.}] ::_thesis: verum
proof
let z be Element of F1(); ::_thesis: ( z in B \/ {.x.} implies S1[z,B \/ {.x.}] )
assume A5: z in B \/ {x} ; ::_thesis: S1[z,B \/ {.x.}]
now__::_thesis:_S1[z,B_\/_{.x.}]
percases ( z in B or z = x ) by A5, ZFMISC_1:136;
suppose z in B ; ::_thesis: S1[z,B \/ {.x.}]
then consider y being Element of F1() such that
A6: y in B and
A7: P1[y,z] and
A8: for x being Element of F1() st x in B & P1[x,y] holds
P1[y,x] by A4;
now__::_thesis:_(_(_P1[x,y]_&_x_in_B_\/_{x}_&_P1[x,z]_&_(_for_v_being_Element_of_F1()_st_v_in_B_\/_{x}_&_P1[v,x]_holds_
P1[x,v]_)_)_or_(_P1[x,y]_&_y_in_B_\/_{x}_&_P1[y,z]_&_(_for_v_being_Element_of_F1()_st_v_in_B_\/_{x}_&_P1[v,y]_holds_
P1[y,v]_)_)_)
percases ( P1[x,y] or not P1[x,y] ) ;
caseA9: P1[x,y] ; ::_thesis: ( x in B \/ {x} & P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus  x in B \/ {x} by ZFMISC_1:136; ::_thesis: ( P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus  P1[x,z] by A2, A7, A9; ::_thesis: for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v]
let v be Element of F1(); ::_thesis: ( v in B \/ {x} & P1[v,x] implies P1[x,v] )
assume that
A10: v in B \/ {x} and
A11: P1[v,x] ; ::_thesis: P1[x,v]
A12: now__::_thesis:_(_v_in_B_implies_P1[x,v]_)
assume A13: v in B ; ::_thesis: P1[x,v]
 P1[v,y] by A2, A9, A11;
then  P1[y,v] by A8, A13;
hence  P1[x,v] by A2, A9; ::_thesis: verum
end;
 ( v in B or v = x ) by A10, ZFMISC_1:136;
hence  P1[x,v] by A1, A12; ::_thesis: verum
end;
caseA14: P1[x,y] ; ::_thesis: ( y in B \/ {x} & P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) )
thus  y in B \/ {x} by A6, XBOOLE_0:def_3; ::_thesis: ( P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) )
thus  P1[y,z] by A7; ::_thesis: for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v]
let v be Element of F1(); ::_thesis: ( v in B \/ {x} & P1[v,y] implies P1[y,v] )
assume that
A15: v in B \/ {x} and
A16: P1[v,y] ; ::_thesis: P1[y,v]
 ( v in B or v = x ) by A15, ZFMISC_1:136;
hence  P1[y,v] by A8, A14, A16; ::_thesis: verum
end;
end;
end;
hence  S1[z,B \/ {.x.}] ; ::_thesis: verum
end;
supposeA17: z = x ; ::_thesis: S1[z,B \/ {.x.}]
now__::_thesis:_(_(_ex_w_being_Element_of_F1()_st_
(_w_in_B_&_P1[w,x]_)_&_ex_u_being_Element_of_F1()_st_
(_u_in_B_\/_{x}_&_P1[u,z]_&_(_for_v_being_Element_of_F1()_st_v_in_B_\/_{x}_&_P1[v,u]_holds_
P1[u,v]_)_)_)_or_(_(_for_w_being_Element_of_F1()_st_w_in_B_holds_
not_P1[w,x]_)_&_x_in_B_\/_{x}_&_P1[x,x]_&_(_for_v_being_Element_of_F1()_st_v_in_B_\/_{x}_&_P1[v,x]_holds_
P1[x,v]_)_)_)
percases ( ex w being Element of F1() st
( w in B & P1[w,x] ) or for w being Element of F1() st w in B holds
not P1[w,x] ) ;
case ex w being Element of F1() st
( w in B & P1[w,x] ) ; ::_thesis: ex u being Element of F1() st
( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )
then consider w being Element of F1() such that
A18: w in B and
A19: P1[w,z] by A17;
consider y being Element of F1() such that
A20: y in B and
A21: P1[y,w] and
A22: for x being Element of F1() st x in B & P1[x,y] holds
P1[y,x] by A4, A18;
take u = y; ::_thesis: ( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )
thus  u in B \/ {x} by A20, XBOOLE_0:def_3; ::_thesis: ( P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )
thus  P1[u,z] by A2, A19, A21; ::_thesis: for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v]
let v be Element of F1(); ::_thesis: ( v in B \/ {x} & P1[v,u] implies P1[u,v] )
assume that
A23: v in B \/ {x} and
A24: P1[v,u] ; ::_thesis: P1[u,v]
 ( v in B or v = x ) by A23, ZFMISC_1:136;
hence  P1[u,v] by A2, A17, A19, A21, A22, A24; ::_thesis: verum
end;
caseA25: for w being Element of F1() st w in B holds
not P1[w,x] ; ::_thesis: ( x in B \/ {x} & P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus  x in B \/ {x} by ZFMISC_1:136; ::_thesis: ( P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus A26: P1[x,x] by A1; ::_thesis: for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v]
let v be Element of F1(); ::_thesis: ( v in B \/ {x} & P1[v,x] implies P1[x,v] )
assume that
A27: v in B \/ {x} and
A28: P1[v,x] ; ::_thesis: P1[x,v]
 not v in B by A25, A28;
hence  P1[x,v] by A26, A27, ZFMISC_1:136; ::_thesis: verum
end;
end;
end;
hence  S1[z,B \/ {.x.}] by A17; ::_thesis: verum
end;
end;
end;
hence  S1[z,B \/ {.x.}] ; ::_thesis: verum
end;
end;
A29: S2[ {}. F1()] ;
 for B being Element of Fin F1() holds S2[B] from SETWISEO:sch_4(A29, A3);
hence  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] ) ) ; ::_thesis: verum
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
defpred S1[ set ] means  ex t9 being Element of F2() st
( t9 in F3() & $1 = F4(t9) & P1[$1,t9] );
set c =  {  F4(t9) where t9 is Element of F2() : t9 in F3()  }  ;
set c1 =  {  tt where tt is Element of F1() : S1[tt]  }  ;
A1:  {  tt where tt is Element of F1() : S1[tt]  }  c=  {  F4(t9) where t9 is Element of F2() : t9 in F3()  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  tt where tt is Element of F1() : S1[tt]  }  or x in  {  F4(t9) where t9 is Element of F2() : t9 in F3()  }  )
assume  x in  {  tt where tt is Element of F1() : S1[tt]  }  ; ::_thesis: x in  {  F4(t9) where t9 is Element of F2() : t9 in F3()  }
then  ex tt being Element of F1() st
( x = tt & ex t9 being Element of F2() st
( t9 in F3() & tt = F4(t9) & P1[tt,t9] ) ) ;
hence  x in  {  F4(t9) where t9 is Element of F2() : t9 in F3()  }  ; ::_thesis: verum
end;
A2:  {  tt where tt is Element of F1() : S1[tt]  }  c= F1() from FRAENKEL:sch_10();
A3: F3() is finite ;
  {  F4(t9) where t9 is Element of F2() : t9 in F3()  }  is finite from FRAENKEL:sch_21(A3);
then reconsider c1 =  {  tt where tt is Element of F1() : S1[tt]  }  as Element of Fin F1() by A1, A2, FINSUB_1:def_5;
take  c1 ; ::_thesis: 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] ) )
let t be Element of F1(); ::_thesis: ( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) )
 ( t in c1 implies ex tt being Element of F1() st
( t = tt & ex t9 being Element of F2() st
( t9 in F3() & tt = F4(t9) & P1[tt,t9] ) ) ) ;
hence  ( t in c1 iff ex t9 being Element of F2() st
( t9 in F3() & t = F4(t9) & P1[t,t9] ) ) ; ::_thesis: verum
end;

registration
let A, B be finite set ;
cluster Funcs (A,B) ->  finite ;
coherence
 Funcs (A,B) is finite
proof
 bool [:A,B:] is finite ;
hence  Funcs (A,B) is finite by Th2, FINSET_1:1; ::_thesis: verum
end;
end;

theorem :: FRAENKEL:6
for A, B being set st A is finite & 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)
proof
defpred S1[ set , set ] means  for phi being Element of Funcs (F1(),F2()) st phi | F3() = $1 holds
$2 = F5(phi);
set Z =  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  ;
set x = the Element of  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  ;
A4: F2() /\ F4() c= F2() by XBOOLE_1:17;
assume A5: not  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  is finite ; ::_thesis: contradiction
then   {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  <> {} ;
then  the Element of  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  in  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  ;
then consider phi being Element of Funcs (F1(),F2()) such that
 the Element of  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  = F5(phi) and
A6: phi .: F3() c= F4() ;
now__::_thesis:_(_F2()_/\_F4()_=_{}_implies_F1()_/\_F3()_=_{}_)
assume  F2() /\ F4() = {} ; ::_thesis: F1() /\ F3() = {}
then A7: phi .: F3() = {} by A6, XBOOLE_1:3, XBOOLE_1:19;
 F1() = dom phi by FUNCT_2:def_1;
then  F1() misses F3() by A7, RELAT_1:118;
hence  F1() /\ F3() = {} by XBOOLE_0:def_7; ::_thesis: verum
end;
then reconsider FF = Funcs ((F1() /\ F3()),(F2() /\ F4())), Z =  {  F5(phi9) where phi9 is Element of Funcs (F1(),F2()) : phi9 .: F3() c= F4()  }  as non empty set by A5, FUNCT_2:8;
A8: F2() /\ F4() c= F4() by XBOOLE_1:17;
A9: F1() /\ F3() c= F1() by XBOOLE_1:17;
A10: now__::_thesis:_for_f_being_Element_of_FF_ex_g_being_Element_of_Z_st_S1[f,g]
let f be Element of FF; ::_thesis: ex g being Element of Z st S1[f,g]
consider phi being Element of Funcs (F1(),F2()) such that
A11: phi | (F1() /\ F3()) = f by A9, A4, Th4;
A12: phi | F3() = f by A11, Th5;
 ex g being Function st
( f = g & dom g = F1() /\ F3() & rng g c= F2() /\ F4() ) by FUNCT_2:def_2;
then  rng (phi | F3()) c= F4() by A8, A12, XBOOLE_1:1;
then  phi .: F3() c= F4() by RELAT_1:115;
then  F5(phi) in Z ;
then reconsider g9 = F5(phi) as Element of Z ;
take g = g9; ::_thesis: S1[f,g]
thus  S1[f,g] by A3, A12; ::_thesis: verum
end;
consider F being Function of FF,Z such that
A13: for f being Element of FF holds S1[f,F . f] from FUNCT_2:sch_3(A10);
 Z c= F .: (Funcs ((F1() /\ F3()),(F2() /\ F4())))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Z or y in F .: (Funcs ((F1() /\ F3()),(F2() /\ F4()))) )
assume  y in Z ; ::_thesis: y in F .: (Funcs ((F1() /\ F3()),(F2() /\ F4())))
then consider phi being Element of Funcs (F1(),F2()) such that
A14: y = F5(phi) and
A15: phi .: F3() c= F4() ;
 rng (phi | F3()) c= F4() by A15, RELAT_1:115;
then A16: rng (phi | F3()) c= F2() /\ F4() by XBOOLE_1:19;
A17: dom (phi | F3()) = (dom phi) /\ F3() by RELAT_1:61
.= F1() /\ F3() by FUNCT_2:def_1 ;
then reconsider x = phi | F3() as Element of Funcs ((F1() /\ F3()),(F2() /\ F4())) by A16, FUNCT_2:def_2;
 phi | F3() in Funcs ((F1() /\ F3()),(F2() /\ F4())) by A17, A16, FUNCT_2:def_2;
then A18: x in dom F by FUNCT_2:def_1;
 y = F . x by A13, A14;
hence  y in F .: (Funcs ((F1() /\ F3()),(F2() /\ F4()))) by A18, FUNCT_1:def_6; ::_thesis: verum
end;
hence  contradiction by A1, A2, A5; ::_thesis: verum
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
set b = the Element of F2();
set M =  {   {  ff where ff is Element of F2() : P1[tt,ff]  }  where tt is Element of F1() : tt in F3()  }  ;
set f = the Function of F1(),F2();
assume A2: for ff being Function of F1(),F2() ex t being Element of F1() st
( t in F3() & P1[t,ff . t] ) ; ::_thesis: contradiction
then consider t being Element of F1() such that
A3: t in F3() and
 P1[t, the Function of F1(),F2() . t] ;
  {  ff where ff is Element of F2() : P1[t,ff]  }  in  {   {  ff where ff is Element of F2() : P1[tt,ff]  }  where tt is Element of F1() : tt in F3()  }  by A3;
then reconsider M =  {   {  ff where ff is Element of F2() : P1[tt,ff]  }  where tt is Element of F1() : tt in F3()  }  as non empty set ;
now__::_thesis:_for_X_being_set_st_X_in_M_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in M implies X <> {} )
assume  X in M ; ::_thesis: X <> {}
then consider t being Element of F1() such that
A4: X =  {  ff where ff is Element of F2() : P1[t,ff]  }  and
A5: t in F3() ;
consider ff being Element of F2() such that
A6: P1[t,ff] by A1, A5;
 ff in X by A4, A6;
hence  X <> {} ; ::_thesis: verum
end;
then consider Choice being Function such that
 dom Choice = M and
A7: for X being set st X in M holds
Choice . X in X by FUNCT_1:111;
defpred S1[ Element of F1(), set ] means ( ( $1 in F3() implies $2 = Choice .  {  ff where ff is Element of F2() : P1[$1,ff]  }  ) & ( $1 in F3() or $2 = the Element of F2() ) );
A8: now__::_thesis:_for_t_being_Element_of_F1()_ex_y_being_Element_of_F2()_st_S1[t,y]
let t be Element of F1(); ::_thesis: ex y being Element of F2() st S1[t,y]
A9: now__::_thesis:_(_t_in_F3()_implies_Choice_.__{__ff_where_ff_is_Element_of_F2()_:_P1[t,ff]__}__is_Element_of_F2()_)
set s =  {  ff where ff is Element of F2() : P1[t,ff]  }  ;
assume  t in F3() ; ::_thesis: Choice .  {  ff where ff is Element of F2() : P1[t,ff]  }  is Element of F2()
then   {  ff where ff is Element of F2() : P1[t,ff]  }  in M ;
then  Choice .  {  ff where ff is Element of F2() : P1[t,ff]  }  in  {  ff where ff is Element of F2() : P1[t,ff]  }  by A7;
then  ex ff being Element of F2() st
( Choice .  {  ff where ff is Element of F2() : P1[t,ff]  }  = ff & P1[t,ff] ) ;
hence  Choice .  {  ff where ff is Element of F2() : P1[t,ff]  }  is Element of F2() ; ::_thesis: verum
end;
 ( t in F3() implies t in F3() ) ;
hence  ex y being Element of F2() st S1[t,y] by A9; ::_thesis: verum
end;
consider f being Function of F1(),F2() such that
A10: for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A8);
now__::_thesis:_for_t_being_Element_of_F1()_st_t_in_F3()_holds_
P1[t,f_._t]
let t be Element of F1(); ::_thesis: ( t in F3() implies P1[t,f . t] )
assume A11: t in F3() ; ::_thesis: P1[t,f . t]
then A12:  {  ff where ff is Element of F2() : P1[t,ff]  }  in M ;
 f . t = Choice .  {  ff where ff is Element of F2() : P1[t,ff]  }  by A10, A11;
then  f . t in  {  ff where ff is Element of F2() : P1[t,ff]  }  by A7, A12;
then  ex ff being Element of F2() st
( f . t = ff & P1[t,ff] ) ;
hence  P1[t,f . t] ; ::_thesis: verum
end;
hence  contradiction by A2; ::_thesis: verum
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
A2: for t being Element of F1() st t in F3() holds
ex ff being Element of F2() st P1[t,ff] by A1;
consider ff being Function of F1(),F2() such that
A3: for t being Element of F1() st t in F3() holds
P1[t,ff . t] from FRAENKEL:sch_26(A2);
reconsider ff = ff as Element of Funcs (F1(),F2()) by FUNCT_2:8;
take  ff ; ::_thesis: for t being Element of F1() st t in F3() holds
P1[t,ff . t]
thus  for t being Element of F1() st t in F3() holds
P1[t,ff . t] by A3; ::_thesis: verum
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
set M =  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  ;
defpred S1[ set , set ] means ( P1[$1,$2] & $1 in F3() & $2 in F2() );
A3: for x, y being set st x in F1() & S1[x,y] holds
y in F2() ;
A4: for x, y1, y2 being set st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2 by A2;
consider f being PartFunc of F1(),F2() such that
A5: for x being set holds
( x in dom f iff ( x in F1() & ex y being set st S1[x,y] ) ) and
A6: for x being set st x in dom f holds
S1[x,f . x] from PARTFUN1:sch_2(A3, A4);
  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  = f .: F3()
proof
thus   {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  c= f .: F3() :: according to XBOOLE_0:def_10 ::_thesis: f .: F3() c=  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  or x in f .: F3() )
assume  x in  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  ; ::_thesis: x in f .: F3()
then consider u being Element of F2() such that
A7: x = u and
A8: ex w being Element of F1() st
( P1[w,u] & w in F3() ) ;
consider w being Element of F1() such that
A9: P1[w,u] and
A10: w in F3() by A8;
A11: w in dom f by A5, A9, A10;
then  S1[w,f . w] by A6;
then  f . w = x by A2, A7, A9;
hence  x in f .: F3() by A10, A11, FUNCT_1:def_6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: F3() or x in  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  )
assume  x in f .: F3() ; ::_thesis: x in  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }
then consider y being set  such that
A12: y in dom f and
A13: y in F3() and
A14: x = f . y by FUNCT_1:def_6;
reconsider x = x as Element of F2() by A6, A12, A14;
 P1[y,x] by A6, A12, A14;
hence  x in  {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  by A12, A13; ::_thesis: verum
end;
hence   {  x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() )  }  is finite by A1; ::_thesis: verum
end;