:: 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;