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