:: WELLFND1 semantic presentation begin theorem Th1: :: WELLFND1:1 for X being functional set st ( for f, g being Function st f in X & g in X holds f tolerates g ) holds union X is Function proof let X be functional set ; ::_thesis: ( ( for f, g being Function st f in X & g in X holds f tolerates g ) implies union X is Function ) assume A1: for f, g being Function st f in X & g in X holds f tolerates g ; ::_thesis: union X is Function A2: union X is Function-like proof let x, y1, y2 be set ; :: according to FUNCT_1:def_1 ::_thesis: ( not [x,y1] in union X or not [x,y2] in union X or y1 = y2 ) assume that A3: [x,y1] in union X and A4: [x,y2] in union X and A5: y1 <> y2 ; ::_thesis: contradiction consider gx being set such that A6: [x,y2] in gx and A7: gx in X by A4, TARSKI:def_4; consider fx being set such that A8: [x,y1] in fx and A9: fx in X by A3, TARSKI:def_4; reconsider fx = fx, gx = gx as Function by A9, A7; fx tolerates gx by A1, A9, A7; then ex h being Function st ( fx c= h & gx c= h ) by PARTFUN1:52; hence contradiction by A5, A8, A6, FUNCT_1:def_1; ::_thesis: verum end; union X is Relation-like proof let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in union X or ex b1, b2 being set st x = [b1,b2] ) assume x in union X ; ::_thesis: ex b1, b2 being set st x = [b1,b2] then ex ux being set st ( x in ux & ux in X ) by TARSKI:def_4; hence ex b1, b2 being set st x = [b1,b2] by RELAT_1:def_1; ::_thesis: verum end; hence union X is Function by A2; ::_thesis: verum end; scheme :: WELLFND1:sch 1 PFSeparation{ F1() -> set , F2() -> set , P1[ set ] } : ex PFS being Subset of (PFuncs (F1(),F2())) st for pfs being PartFunc of F1(),F2() holds ( pfs in PFS iff P1[pfs] ) proof consider fs being Subset of (PFuncs (F1(),F2())) such that A1: for f being set holds ( f in fs iff ( f in PFuncs (F1(),F2()) & P1[f] ) ) from SUBSET_1:sch_1(); take fs ; ::_thesis: for pfs being PartFunc of F1(),F2() holds ( pfs in fs iff P1[pfs] ) let pfs be PartFunc of F1(),F2(); ::_thesis: ( pfs in fs iff P1[pfs] ) pfs in PFuncs (F1(),F2()) by PARTFUN1:45; hence ( pfs in fs iff P1[pfs] ) by A1; ::_thesis: verum end; registration let X be set ; cluster nextcard X -> non empty ; coherence not nextcard X is empty by CARD_1:def_3; end; registration cluster non empty epsilon-transitive epsilon-connected ordinal non finite cardinal regular for set ; existence ex b1 being Aleph st b1 is regular by CARD_5:30; end; theorem Th2: :: WELLFND1:2 for M being regular Aleph for X being set st X c= M & card X in M holds sup X in M proof let M be regular Aleph; ::_thesis: for X being set st X c= M & card X in M holds sup X in M cf M = M by CARD_5:def_3; hence for X being set st X c= M & card X in M holds sup X in M by CARD_5:26; ::_thesis: verum end; theorem Th3: :: WELLFND1:3 for R being RelStr for x being set holds the InternalRel of R -Seg x c= the carrier of R proof let R be RelStr ; ::_thesis: for x being set holds the InternalRel of R -Seg x c= the carrier of R let x be set ; ::_thesis: the InternalRel of R -Seg x c= the carrier of R set r = the InternalRel of R; set c = the carrier of R; ( the InternalRel of R -Seg x c= field the InternalRel of R & field the InternalRel of R c= the carrier of R \/ the carrier of R ) by RELSET_1:8, WELLORD1:9; hence the InternalRel of R -Seg x c= the carrier of R by XBOOLE_1:1; ::_thesis: verum end; definition let R be RelStr ; let X be Subset of R; redefine attr X is lower means :Def1: :: WELLFND1:def 1 for x, y being set st x in X & [y,x] in the InternalRel of R holds y in X; compatibility ( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds y in X ) proof hereby ::_thesis: ( ( for x, y being set st x in X & [y,x] in the InternalRel of R holds y in X ) implies X is lower ) assume A1: X is lower ; ::_thesis: for x, y being set st x in X & [y,x] in the InternalRel of R holds y in X let x, y be set ; ::_thesis: ( x in X & [y,x] in the InternalRel of R implies y in X ) assume that A2: x in X and A3: [y,x] in the InternalRel of R ; ::_thesis: y in X reconsider x9 = x, y9 = y as Element of R by A3, ZFMISC_1:87; y9 <= x9 by A3, ORDERS_2:def_5; hence y in X by A1, A2, WAYBEL_0:def_19; ::_thesis: verum end; assume A4: for x, y being set st x in X & [y,x] in the InternalRel of R holds y in X ; ::_thesis: X is lower let x, y be Element of R; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in X or not y <= x or y in X ) assume A5: x in X ; ::_thesis: ( not y <= x or y in X ) assume y <= x ; ::_thesis: y in X then [y,x] in the InternalRel of R by ORDERS_2:def_5; hence y in X by A4, A5; ::_thesis: verum end; end; :: deftheorem Def1 defines lower WELLFND1:def_1_:_ for R being RelStr for X being Subset of R holds ( X is lower iff for x, y being set st x in X & [y,x] in the InternalRel of R holds y in X ); theorem Th4: :: WELLFND1:4 for R being RelStr for X being Subset of R for x being set st X is lower & x in X holds the InternalRel of R -Seg x c= X proof let R be RelStr ; ::_thesis: for X being Subset of R for x being set st X is lower & x in X holds the InternalRel of R -Seg x c= X let X be Subset of R; ::_thesis: for x being set st X is lower & x in X holds the InternalRel of R -Seg x c= X let x be set ; ::_thesis: ( X is lower & x in X implies the InternalRel of R -Seg x c= X ) assume A1: ( X is lower & x in X ) ; ::_thesis: the InternalRel of R -Seg x c= X let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the InternalRel of R -Seg x or z in X ) assume z in the InternalRel of R -Seg x ; ::_thesis: z in X then [z,x] in the InternalRel of R by WELLORD1:1; hence z in X by A1, Def1; ::_thesis: verum end; theorem Th5: :: WELLFND1:5 for R being RelStr for X being lower Subset of R for Y being Subset of R for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds Y is lower proof let R be RelStr ; ::_thesis: for X being lower Subset of R for Y being Subset of R for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds Y is lower let X be lower Subset of R; ::_thesis: for Y being Subset of R for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds Y is lower let Y be Subset of R; ::_thesis: for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds Y is lower let x be set ; ::_thesis: ( Y = X \/ {x} & the InternalRel of R -Seg x c= X implies Y is lower ) set r = the InternalRel of R; assume that A1: Y = X \/ {x} and A2: the InternalRel of R -Seg x c= X ; ::_thesis: Y is lower let z, y be set ; :: according to WELLFND1:def_1 ::_thesis: ( z in Y & [y,z] in the InternalRel of R implies y in Y ) assume that A3: z in Y and A4: [y,z] in the InternalRel of R ; ::_thesis: y in Y percases ( z in X or ( z in {x} & y = z ) or ( z in {x} & y <> z ) ) by A1, A3, XBOOLE_0:def_3; suppose z in X ; ::_thesis: y in Y then y in X by A4, Def1; hence y in Y by A1, XBOOLE_0:def_3; ::_thesis: verum end; suppose ( z in {x} & y = z ) ; ::_thesis: y in Y hence y in Y by A3; ::_thesis: verum end; supposeA5: ( z in {x} & y <> z ) ; ::_thesis: y in Y then z = x by TARSKI:def_1; then y in the InternalRel of R -Seg x by A4, A5, WELLORD1:1; hence y in Y by A1, A2, XBOOLE_0:def_3; ::_thesis: verum end; end; end; begin definition let R be RelStr ; attrR is well_founded means :Def2: :: WELLFND1:def 2 the InternalRel of R is_well_founded_in the carrier of R; end; :: deftheorem Def2 defines well_founded WELLFND1:def_2_:_ for R being RelStr holds ( R is well_founded iff the InternalRel of R is_well_founded_in the carrier of R ); registration cluster non empty well_founded for RelStr ; existence ex b1 being RelStr st ( not b1 is empty & b1 is well_founded ) proof reconsider er = {} as Relation of {{}} by RELSET_1:12; take R = RelStr(# {{}},er #); ::_thesis: ( not R is empty & R is well_founded ) thus not R is empty ; ::_thesis: R is well_founded let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_2 ::_thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ) assume A1: ( Y c= the carrier of R & Y <> {} ) ; ::_thesis: ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) take e = {} ; ::_thesis: ( e in Y & the InternalRel of R -Seg e misses Y ) Y = {{}} by A1, ZFMISC_1:33; hence e in Y by TARSKI:def_1; ::_thesis: the InternalRel of R -Seg e misses Y assume ( the InternalRel of R -Seg e) /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A2: x in ( the InternalRel of R -Seg e) /\ Y by XBOOLE_0:def_1; x in the InternalRel of R -Seg e by A2, XBOOLE_0:def_4; hence contradiction by WELLORD1:1; ::_thesis: verum end; end; definition let R be RelStr ; let X be Subset of R; attrX is well_founded means :Def3: :: WELLFND1:def 3 the InternalRel of R is_well_founded_in X; end; :: deftheorem Def3 defines well_founded WELLFND1:def_3_:_ for R being RelStr for X being Subset of R holds ( X is well_founded iff the InternalRel of R is_well_founded_in X ); registration let R be RelStr ; cluster well_founded for Element of bool the carrier of R; existence ex b1 being Subset of R st b1 is well_founded proof reconsider e = {} as Subset of R by XBOOLE_1:2; take e ; ::_thesis: e is well_founded let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Y c= e or Y = {} or ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ) assume ( Y c= e & Y <> {} ) ; ::_thesis: ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) hence ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ; ::_thesis: verum end; end; definition let R be RelStr ; func well_founded-Part R -> Subset of R means :Def4: :: WELLFND1:def 4 it = union { S where S is Subset of R : ( S is well_founded & S is lower ) } ; existence ex b1 being Subset of R st b1 = union { S where S is Subset of R : ( S is well_founded & S is lower ) } proof set IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } ; { S where S is Subset of R : ( S is well_founded & S is lower ) } c= bool the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { S where S is Subset of R : ( S is well_founded & S is lower ) } or x in bool the carrier of R ) assume x in { S where S is Subset of R : ( S is well_founded & S is lower ) } ; ::_thesis: x in bool the carrier of R then ex S being Subset of R st ( x = S & S is well_founded & S is lower ) ; hence x in bool the carrier of R ; ::_thesis: verum end; then reconsider IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } as Subset-Family of R ; union IT is Subset of R ; hence ex b1 being Subset of R st b1 = union { S where S is Subset of R : ( S is well_founded & S is lower ) } ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of R st b1 = union { S where S is Subset of R : ( S is well_founded & S is lower ) } & b2 = union { S where S is Subset of R : ( S is well_founded & S is lower ) } holds b1 = b2 ; end; :: deftheorem Def4 defines well_founded-Part WELLFND1:def_4_:_ for R being RelStr for b2 being Subset of R holds ( b2 = well_founded-Part R iff b2 = union { S where S is Subset of R : ( S is well_founded & S is lower ) } ); registration let R be RelStr ; cluster well_founded-Part R -> lower well_founded ; coherence ( well_founded-Part R is lower & well_founded-Part R is well_founded ) proof set wfp = well_founded-Part R; set r = the InternalRel of R; set IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } ; A1: well_founded-Part R = union { S where S is Subset of R : ( S is well_founded & S is lower ) } by Def4; hereby :: according to WELLFND1:def_1 ::_thesis: well_founded-Part R is well_founded let x, y be set ; ::_thesis: ( x in well_founded-Part R & [y,x] in the InternalRel of R implies y in well_founded-Part R ) assume that A2: x in well_founded-Part R and A3: [y,x] in the InternalRel of R ; ::_thesis: y in well_founded-Part R consider Y being set such that A4: x in Y and A5: Y in { S where S is Subset of R : ( S is well_founded & S is lower ) } by A1, A2, TARSKI:def_4; consider S being Subset of R such that A6: Y = S and A7: ( S is well_founded & S is lower ) by A5; y in S by A3, A4, A6, A7, Def1; hence y in well_founded-Part R by A1, A5, A6, TARSKI:def_4; ::_thesis: verum end; let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Y c= well_founded-Part R or Y = {} or ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ) assume that A8: Y c= well_founded-Part R and A9: Y <> {} ; ::_thesis: ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) consider y being set such that A10: y in Y by A9, XBOOLE_0:def_1; consider YY being set such that A11: y in YY and A12: YY in { S where S is Subset of R : ( S is well_founded & S is lower ) } by A1, A8, A10, TARSKI:def_4; consider S being Subset of R such that A13: YY = S and A14: ( S is well_founded & S is lower ) by A12; set YS = Y /\ S; A15: the InternalRel of R is_well_founded_in S by A14, Def3; ( Y /\ S c= S & Y /\ S <> {} ) by A10, A11, A13, XBOOLE_0:def_4, XBOOLE_1:17; then consider a being set such that A16: a in Y /\ S and A17: the InternalRel of R -Seg a misses Y /\ S by A15, WELLORD1:def_3; A18: a in Y by A16, XBOOLE_0:def_4; a in S by A16, XBOOLE_0:def_4; then A19: ( the InternalRel of R -Seg a) /\ Y = (( the InternalRel of R -Seg a) /\ S) /\ Y by A14, Th4, XBOOLE_1:28 .= ( the InternalRel of R -Seg a) /\ (Y /\ S) by XBOOLE_1:16 ; ( the InternalRel of R -Seg a) /\ (Y /\ S) = {} by A17, XBOOLE_0:def_7; then the InternalRel of R -Seg a misses Y by A19, XBOOLE_0:def_7; hence ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) by A18; ::_thesis: verum end; end; theorem Th6: :: WELLFND1:6 for R being non empty RelStr for x being Element of R holds {x} is well_founded Subset of R proof let R be non empty RelStr ; ::_thesis: for x being Element of R holds {x} is well_founded Subset of R let x be Element of R; ::_thesis: {x} is well_founded Subset of R set r = the InternalRel of R; reconsider sx = {x} as Subset of R ; sx is well_founded proof let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Y c= sx or Y = {} or ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ) assume that A1: Y c= sx and A2: Y <> {} ; ::_thesis: ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) take x ; ::_thesis: ( x in Y & the InternalRel of R -Seg x misses Y ) Y = sx by A1, A2, ZFMISC_1:33; hence x in Y by TARSKI:def_1; ::_thesis: the InternalRel of R -Seg x misses Y assume not the InternalRel of R -Seg x misses Y ; ::_thesis: contradiction then consider a being set such that A3: a in ( the InternalRel of R -Seg x) /\ Y by XBOOLE_0:4; a in the InternalRel of R -Seg x by A3, XBOOLE_0:def_4; then A4: a <> x by WELLORD1:1; a in Y by A3, XBOOLE_0:def_4; hence contradiction by A1, A4, TARSKI:def_1; ::_thesis: verum end; hence {x} is well_founded Subset of R ; ::_thesis: verum end; theorem Th7: :: WELLFND1:7 for R being RelStr for X, Y being well_founded Subset of R st X is lower holds X \/ Y is well_founded Subset of R proof let R be RelStr ; ::_thesis: for X, Y being well_founded Subset of R st X is lower holds X \/ Y is well_founded Subset of R let X, Y be well_founded Subset of R; ::_thesis: ( X is lower implies X \/ Y is well_founded Subset of R ) set r = the InternalRel of R; assume A1: X is lower ; ::_thesis: X \/ Y is well_founded Subset of R reconsider XY = X \/ Y as Subset of R ; A2: the InternalRel of R is_well_founded_in Y by Def3; A3: the InternalRel of R is_well_founded_in X by Def3; XY is well_founded proof let Z be set ; :: according to WELLORD1:def_3,WELLFND1:def_3 ::_thesis: ( not Z c= XY or Z = {} or ex b1 being set st ( b1 in Z & the InternalRel of R -Seg b1 misses Z ) ) assume that A4: Z c= XY and A5: Z <> {} ; ::_thesis: ex b1 being set st ( b1 in Z & the InternalRel of R -Seg b1 misses Z ) set XZ = X /\ Z; A6: X /\ Z c= X by XBOOLE_1:17; percases ( X /\ Z = {} or X /\ Z <> {} ) ; suppose X /\ Z = {} ; ::_thesis: ex b1 being set st ( b1 in Z & the InternalRel of R -Seg b1 misses Z ) then X misses Z by XBOOLE_0:def_7; then Z c= Y by A4, XBOOLE_1:73; hence ex b1 being set st ( b1 in Z & the InternalRel of R -Seg b1 misses Z ) by A2, A5, WELLORD1:def_3; ::_thesis: verum end; suppose X /\ Z <> {} ; ::_thesis: ex b1 being set st ( b1 in Z & the InternalRel of R -Seg b1 misses Z ) then consider a being set such that A7: a in X /\ Z and A8: the InternalRel of R -Seg a misses X /\ Z by A3, A6, WELLORD1:def_3; A9: a in X by A7, XBOOLE_0:def_4; take a ; ::_thesis: ( a in Z & the InternalRel of R -Seg a misses Z ) thus a in Z by A7, XBOOLE_0:def_4; ::_thesis: the InternalRel of R -Seg a misses Z assume ( the InternalRel of R -Seg a) /\ Z <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider b being set such that A10: b in ( the InternalRel of R -Seg a) /\ Z by XBOOLE_0:def_1; A11: b in Z by A10, XBOOLE_0:def_4; A12: b in the InternalRel of R -Seg a by A10, XBOOLE_0:def_4; then [b,a] in the InternalRel of R by WELLORD1:1; then b in X by A1, A9, Def1; then b in X /\ Z by A11, XBOOLE_0:def_4; hence contradiction by A8, A12, XBOOLE_0:3; ::_thesis: verum end; end; end; hence X \/ Y is well_founded Subset of R ; ::_thesis: verum end; theorem Th8: :: WELLFND1:8 for R being RelStr holds ( R is well_founded iff well_founded-Part R = the carrier of R ) proof let R be RelStr ; ::_thesis: ( R is well_founded iff well_founded-Part R = the carrier of R ) set r = the InternalRel of R; set c = the carrier of R; set wfp = well_founded-Part R; set IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } ; the carrier of R c= the carrier of R ; then reconsider cs = the carrier of R as Subset of R ; A1: well_founded-Part R = union { S where S is Subset of R : ( S is well_founded & S is lower ) } by Def4; hereby ::_thesis: ( well_founded-Part R = the carrier of R implies R is well_founded ) A2: cs is lower proof let x, y be set ; :: according to WELLFND1:def_1 ::_thesis: ( x in cs & [y,x] in the InternalRel of R implies y in cs ) thus ( x in cs & [y,x] in the InternalRel of R implies y in cs ) by ZFMISC_1:87; ::_thesis: verum end; assume R is well_founded ; ::_thesis: well_founded-Part R = the carrier of R then the InternalRel of R is_well_founded_in cs by Def2; then cs is well_founded by Def3; then cs in { S where S is Subset of R : ( S is well_founded & S is lower ) } by A2; then cs c= well_founded-Part R by A1, ZFMISC_1:74; hence well_founded-Part R = the carrier of R by XBOOLE_0:def_10; ::_thesis: verum end; assume A3: well_founded-Part R = the carrier of R ; ::_thesis: R is well_founded let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_2 ::_thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ) assume that A4: Y c= the carrier of R and A5: Y <> {} ; ::_thesis: ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) consider y being set such that A6: y in Y by A5, XBOOLE_0:def_1; consider YY being set such that A7: y in YY and A8: YY in { S where S is Subset of R : ( S is well_founded & S is lower ) } by A1, A3, A4, A6, TARSKI:def_4; consider S being Subset of R such that A9: YY = S and A10: ( S is well_founded & S is lower ) by A8; set YS = Y /\ S; A11: the InternalRel of R is_well_founded_in S by A10, Def3; ( Y /\ S c= S & Y /\ S <> {} ) by A6, A7, A9, XBOOLE_0:def_4, XBOOLE_1:17; then consider a being set such that A12: a in Y /\ S and A13: the InternalRel of R -Seg a misses Y /\ S by A11, WELLORD1:def_3; A14: a in Y by A12, XBOOLE_0:def_4; a in S by A12, XBOOLE_0:def_4; then A15: ( the InternalRel of R -Seg a) /\ Y = (( the InternalRel of R -Seg a) /\ S) /\ Y by A10, Th4, XBOOLE_1:28 .= ( the InternalRel of R -Seg a) /\ (Y /\ S) by XBOOLE_1:16 ; ( the InternalRel of R -Seg a) /\ (Y /\ S) = {} by A13, XBOOLE_0:def_7; then the InternalRel of R -Seg a misses Y by A15, XBOOLE_0:def_7; hence ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) by A14; ::_thesis: verum end; theorem Th9: :: WELLFND1:9 for R being non empty RelStr for x being Element of R st the InternalRel of R -Seg x c= well_founded-Part R holds x in well_founded-Part R proof let R be non empty RelStr ; ::_thesis: for x being Element of R st the InternalRel of R -Seg x c= well_founded-Part R holds x in well_founded-Part R let x be Element of R; ::_thesis: ( the InternalRel of R -Seg x c= well_founded-Part R implies x in well_founded-Part R ) set wfp = well_founded-Part R; set IT = { S where S is Subset of R : ( S is well_founded & S is lower ) } ; set xwfp = (well_founded-Part R) \/ {x}; A1: well_founded-Part R = union { S where S is Subset of R : ( S is well_founded & S is lower ) } by Def4; x in {x} by TARSKI:def_1; then A2: x in (well_founded-Part R) \/ {x} by XBOOLE_0:def_3; reconsider xwfp = (well_founded-Part R) \/ {x} as Subset of R ; {x} is well_founded Subset of R by Th6; then A3: xwfp is well_founded by Th7; assume the InternalRel of R -Seg x c= well_founded-Part R ; ::_thesis: x in well_founded-Part R then xwfp is lower by Th5; then xwfp in { S where S is Subset of R : ( S is well_founded & S is lower ) } by A3; hence x in well_founded-Part R by A1, A2, TARSKI:def_4; ::_thesis: verum end; scheme :: WELLFND1:sch 2 WFMin{ F1() -> non empty RelStr , F2() -> Element of F1(), P1[ set ] } : ex x being Element of F1() st ( P1[x] & ( for y being Element of F1() holds ( not x <> y or not P1[y] or not [y,x] in the InternalRel of F1() ) ) ) provided A1: P1[F2()] and A2: F1() is well_founded proof set c = the carrier of F1(); set r = the InternalRel of F1(); set Z = { x where x is Element of the carrier of F1() : P1[x] } ; A3: F2() in { x where x is Element of the carrier of F1() : P1[x] } by A1; { x where x is Element of the carrier of F1() : P1[x] } is Subset of the carrier of F1() from DOMAIN_1:sch_7(); then reconsider Z = { x where x is Element of the carrier of F1() : P1[x] } as non empty Subset of the carrier of F1() by A3; the InternalRel of F1() is_well_founded_in the carrier of F1() by A2, Def2; then consider a being set such that A4: a in Z and A5: the InternalRel of F1() -Seg a misses Z by WELLORD1:def_3; reconsider a = a as Element of F1() by A4; take a ; ::_thesis: ( P1[a] & ( for y being Element of F1() holds ( not a <> y or not P1[y] or not [y,a] in the InternalRel of F1() ) ) ) ex a9 being Element of the carrier of F1() st ( a9 = a & P1[a9] ) by A4; hence P1[a] ; ::_thesis: for y being Element of F1() holds ( not a <> y or not P1[y] or not [y,a] in the InternalRel of F1() ) given y being Element of F1() such that A6: ( a <> y & P1[y] & [y,a] in the InternalRel of F1() ) ; ::_thesis: contradiction ( y in Z & y in the InternalRel of F1() -Seg a ) by A6, WELLORD1:1; hence contradiction by A5, XBOOLE_0:3; ::_thesis: verum end; theorem Th10: :: WELLFND1:10 for R being non empty RelStr holds ( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds x in S ) holds the carrier of R c= S ) proof let R be non empty RelStr ; ::_thesis: ( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds x in S ) holds the carrier of R c= S ) set c = the carrier of R; set r = the InternalRel of R; hereby ::_thesis: ( ( for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds x in S ) holds the carrier of R c= S ) implies R is well_founded ) assume A1: R is well_founded ; ::_thesis: for S being set st ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds x in S ) holds the carrier of R c= S let S be set ; ::_thesis: ( ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds x in S ) implies the carrier of R c= S ) assume A2: for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds x in S ; ::_thesis: the carrier of R c= S defpred S1[ set ] means ( \$1 in the carrier of R & not \$1 in S ); assume not the carrier of R c= S ; ::_thesis: contradiction then consider x being set such that A3: x in the carrier of R and A4: not x in S by TARSKI:def_3; reconsider x = x as Element of R by A3; A5: S1[x] by A4; consider x0 being Element of R such that A6: S1[x0] and A7: for y being Element of R holds ( not x0 <> y or not S1[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A5, A1); now__::_thesis:_the_InternalRel_of_R_-Seg_x0_c=_S assume not the InternalRel of R -Seg x0 c= S ; ::_thesis: contradiction then consider z being set such that A8: z in the InternalRel of R -Seg x0 and A9: not z in S by TARSKI:def_3; A10: x0 <> z by A8, WELLORD1:1; A11: [z,x0] in the InternalRel of R by A8, WELLORD1:1; then reconsider z = z as Element of R by ZFMISC_1:87; z = z ; hence contradiction by A7, A9, A10, A11; ::_thesis: verum end; hence contradiction by A2, A6; ::_thesis: verum end; assume A12: for S being set st ( for x being Element of the carrier of R st the InternalRel of R -Seg x c= S holds x in S ) holds the carrier of R c= S ; ::_thesis: R is well_founded assume not R is well_founded ; ::_thesis: contradiction then not the InternalRel of R is_well_founded_in the carrier of R by Def2; then consider Y being set such that A13: ( Y c= the carrier of R & Y <> {} ) and A14: for a being set holds ( not a in Y or not the InternalRel of R -Seg a misses Y ) by WELLORD1:def_3; now__::_thesis:_for_x_being_Element_of_the_carrier_of_R_st_the_InternalRel_of_R_-Seg_x_c=_the_carrier_of_R_\_Y_holds_ x_in_the_carrier_of_R_\_Y let x be Element of the carrier of R; ::_thesis: ( the InternalRel of R -Seg x c= the carrier of R \ Y implies x in the carrier of R \ Y ) assume A15: the InternalRel of R -Seg x c= the carrier of R \ Y ; ::_thesis: x in the carrier of R \ Y assume not x in the carrier of R \ Y ; ::_thesis: contradiction then x in Y by XBOOLE_0:def_5; then the InternalRel of R -Seg x meets Y by A14; then ex z being set st ( z in the InternalRel of R -Seg x & z in Y ) by XBOOLE_0:3; hence contradiction by A15, XBOOLE_0:def_5; ::_thesis: verum end; then the carrier of R c= the carrier of R \ Y by A12; hence contradiction by A13, XBOOLE_1:1, XBOOLE_1:38; ::_thesis: verum end; scheme :: WELLFND1:sch 3 WFInduction{ F1() -> non empty RelStr , P1[ set ] } : for x being Element of F1() holds P1[x] provided A1: for x being Element of F1() st ( for y being Element of F1() st y <> x & [y,x] in the InternalRel of F1() holds P1[y] ) holds P1[x] and A2: F1() is well_founded proof set c = the carrier of F1(); set r = the InternalRel of F1(); set Z = { x where x is Element of the carrier of F1() : P1[x] } ; now__::_thesis:_for_x_being_Element_of_the_carrier_of_F1()_st_the_InternalRel_of_F1()_-Seg_x_c=__{__x_where_x_is_Element_of_the_carrier_of_F1()_:_P1[x]__}__holds_ x_in__{__x_where_x_is_Element_of_the_carrier_of_F1()_:_P1[x]__}_ let x be Element of the carrier of F1(); ::_thesis: ( the InternalRel of F1() -Seg x c= { x where x is Element of the carrier of F1() : P1[x] } implies x in { x where x is Element of the carrier of F1() : P1[x] } ) assume A3: the InternalRel of F1() -Seg x c= { x where x is Element of the carrier of F1() : P1[x] } ; ::_thesis: x in { x where x is Element of the carrier of F1() : P1[x] } reconsider x9 = x as Element of F1() ; now__::_thesis:_for_y9_being_Element_of_F1()_st_y9_<>_x9_&_[y9,x9]_in_the_InternalRel_of_F1()_holds_ P1[y9] let y9 be Element of F1(); ::_thesis: ( y9 <> x9 & [y9,x9] in the InternalRel of F1() implies P1[y9] ) assume ( y9 <> x9 & [y9,x9] in the InternalRel of F1() ) ; ::_thesis: P1[y9] then y9 in the InternalRel of F1() -Seg x9 by WELLORD1:1; then y9 in { x where x is Element of the carrier of F1() : P1[x] } by A3; then ex y being Element of the carrier of F1() st ( y = y9 & P1[y] ) ; hence P1[y9] ; ::_thesis: verum end; then P1[x9] by A1; hence x in { x where x is Element of the carrier of F1() : P1[x] } ; ::_thesis: verum end; then A4: the carrier of F1() c= { x where x is Element of the carrier of F1() : P1[x] } by A2, Th10; let x be Element of F1(); ::_thesis: P1[x] x in the carrier of F1() ; then x in { x where x is Element of the carrier of F1() : P1[x] } by A4; then ex x9 being Element of the carrier of F1() st ( x = x9 & P1[x9] ) ; hence P1[x] ; ::_thesis: verum end; definition let R be non empty RelStr ; let V be non empty set ; let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; let F be Function; predF is_recursively_expressed_by H means :Def5: :: WELLFND1:def 5 for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x))); end; :: deftheorem Def5 defines is_recursively_expressed_by WELLFND1:def_5_:_ for R being non empty RelStr for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F being Function holds ( F is_recursively_expressed_by H iff for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x))) ); theorem :: WELLFND1:11 for R being non empty RelStr holds ( R is well_founded iff for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H ) proof let R be non empty RelStr ; ::_thesis: ( R is well_founded iff for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H ) set c = the carrier of R; set r = the InternalRel of R; defpred S1[] means for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H; reconsider ac = omega +` (card the carrier of R) as infinite Cardinal ; set V = nextcard ac; deffunc H1( Element of the carrier of R, Element of PFuncs ( the carrier of R,(nextcard ac))) -> set = sup (rng \$2); A1: for x being Element of the carrier of R for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H1(x,p) in nextcard ac proof let x be Element of the carrier of R; ::_thesis: for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H1(x,p) in nextcard ac let p be Element of PFuncs ( the carrier of R,(nextcard ac)); ::_thesis: H1(x,p) in nextcard ac ( card (dom p) c= card the carrier of R & card (rng p) c= card (dom p) ) by CARD_1:11, CARD_1:12; then A2: card (rng p) c= card the carrier of R by XBOOLE_1:1; card the carrier of R c= ac by CARD_2:94; then card (rng p) c= ac by A2, XBOOLE_1:1; then A3: card (rng p) in nextcard ac by CARD_1:18, ORDINAL1:12; nextcard ac is regular by CARD_5:30; hence H1(x,p) in nextcard ac by A3, Th2; ::_thesis: verum end; consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,(nextcard ac))):],(nextcard ac) such that A4: for x being Element of the carrier of R for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H . (x,p) = H1(x,p) from FUNCT_7:sch_1(A1); thus ( R is well_founded implies S1[] ) ::_thesis: ( ( for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H ) implies R is well_founded ) proof assume A5: R is well_founded ; ::_thesis: S1[] let V be non empty set ; ::_thesis: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; ::_thesis: ex F being Function of the carrier of R,V st F is_recursively_expressed_by H defpred S2[ PartFunc of the carrier of R,V] means ( dom \$1 is lower & ( for x being set st x in dom \$1 holds \$1 . x = H . [x,(\$1 | ( the InternalRel of R -Seg x))] ) ); consider fs being Subset of (PFuncs ( the carrier of R,V)) such that A6: for f being PartFunc of the carrier of R,V holds ( f in fs iff S2[f] ) from WELLFND1:sch_1(); now__::_thesis:_for_f,_g_being_Function_st_f_in_fs_&_g_in_fs_holds_ f_tolerates_g let f, g be Function; ::_thesis: ( f in fs & g in fs implies f tolerates g ) assume that A7: f in fs and A8: g in fs ; ::_thesis: f tolerates g reconsider ff = f, gg = g as PartFunc of the carrier of R,V by A7, A8, PARTFUN1:46; defpred S3[ set ] means ( \$1 in dom ff & \$1 in dom gg & ff . \$1 <> gg . \$1 ); assume not f tolerates g ; ::_thesis: contradiction then consider x being set such that A9: x in (dom ff) /\ (dom gg) and A10: ff . x <> gg . x by PARTFUN1:def_4; reconsider x = x as Element of R by A9; A11: S3[x] by A9, A10, XBOOLE_0:def_4; consider x0 being Element of R such that A12: S3[x0] and A13: for y being Element of R holds ( not x0 <> y or not S3[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A11, A5); ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0) proof set fr = ff | ( the InternalRel of R -Seg x0); set gr = gg | ( the InternalRel of R -Seg x0); assume A14: not ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0) ; ::_thesis: contradiction A15: dom ff is lower by A6, A7; then A16: dom (ff | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by A12, Th4, RELAT_1:62; A17: dom gg is lower by A6, A8; then dom (ff | ( the InternalRel of R -Seg x0)) = dom (gg | ( the InternalRel of R -Seg x0)) by A12, A16, Th4, RELAT_1:62; then consider x1 being set such that A18: x1 in dom (ff | ( the InternalRel of R -Seg x0)) and A19: (ff | ( the InternalRel of R -Seg x0)) . x1 <> (gg | ( the InternalRel of R -Seg x0)) . x1 by A14, FUNCT_1:2; A20: [x1,x0] in the InternalRel of R by A16, A18, WELLORD1:1; reconsider x1 = x1 as Element of R by A18; A21: ( (ff | ( the InternalRel of R -Seg x0)) . x1 = ff . x1 & (gg | ( the InternalRel of R -Seg x0)) . x1 = gg . x1 ) by A16, A18, FUNCT_1:49; A22: x1 <> x0 by A16, A18, WELLORD1:1; A23: x1 in dom gg by A12, A17, A20, Def1; x1 in dom ff by A12, A15, A20, Def1; hence contradiction by A13, A19, A20, A21, A22, A23; ::_thesis: verum end; then ff . x0 = H . [x0,(gg | ( the InternalRel of R -Seg x0))] by A6, A7, A12 .= gg . x0 by A6, A8, A12 ; hence contradiction by A12; ::_thesis: verum end; then reconsider ufs = union fs as Function by Th1; A24: now__::_thesis:_for_x_being_set_st_x_in_dom_ufs_holds_ ufs_._x_=_H_._[x,(ufs_|_(_the_InternalRel_of_R_-Seg_x))] let x be set ; ::_thesis: ( x in dom ufs implies ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))] ) assume x in dom ufs ; ::_thesis: ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))] then [x,(ufs . x)] in ufs by FUNCT_1:1; then consider fx being set such that A25: [x,(ufs . x)] in fx and A26: fx in fs by TARSKI:def_4; reconsider ff = fx as PartFunc of the carrier of R,V by A26, PARTFUN1:46; A27: x in dom ff by A25, FUNCT_1:1; A28: ( dom ff is lower & ff c= ufs ) by A6, A26, ZFMISC_1:74; thus ufs . x = ff . x by A25, FUNCT_1:1 .= H . [x,(ff | ( the InternalRel of R -Seg x))] by A6, A26, A27 .= H . [x,(ufs | ( the InternalRel of R -Seg x))] by A27, A28, Th4, GRFUNC_1:27 ; ::_thesis: verum end; A29: dom ufs c= the carrier of R proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom ufs or y in the carrier of R ) assume y in dom ufs ; ::_thesis: y in the carrier of R then [y,(ufs . y)] in ufs by FUNCT_1:1; then consider fx being set such that A30: [y,(ufs . y)] in fx and A31: fx in fs by TARSKI:def_4; consider ff being Function such that A32: ff = fx and A33: dom ff c= the carrier of R and rng ff c= V by A31, PARTFUN1:def_3; y in dom ff by A30, A32, XTUPLE_0:def_12; hence y in the carrier of R by A33; ::_thesis: verum end; A34: rng ufs c= V proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ufs or y in V ) assume y in rng ufs ; ::_thesis: y in V then consider x being set such that A35: ( x in dom ufs & y = ufs . x ) by FUNCT_1:def_3; [x,y] in ufs by A35, FUNCT_1:1; then consider fx being set such that A36: [x,y] in fx and A37: fx in fs by TARSKI:def_4; consider ff being Function such that A38: ff = fx and dom ff c= the carrier of R and A39: rng ff c= V by A37, PARTFUN1:def_3; y in rng ff by A36, A38, XTUPLE_0:def_13; hence y in V by A39; ::_thesis: verum end; A40: now__::_thesis:_for_x,_y_being_set_st_x_in_dom_ufs_&_[y,x]_in_the_InternalRel_of_R_holds_ y_in_dom_ufs let x, y be set ; ::_thesis: ( x in dom ufs & [y,x] in the InternalRel of R implies y in dom ufs ) assume that A41: x in dom ufs and A42: [y,x] in the InternalRel of R ; ::_thesis: y in dom ufs [x,(ufs . x)] in ufs by A41, FUNCT_1:1; then consider fx being set such that A43: [x,(ufs . x)] in fx and A44: fx in fs by TARSKI:def_4; reconsider ff = fx as PartFunc of the carrier of R,V by A44, PARTFUN1:46; ff c= ufs by A44, ZFMISC_1:74; then A45: dom ff c= dom ufs by GRFUNC_1:2; ( dom ff is lower & x in dom ff ) by A6, A43, A44, FUNCT_1:1; then y in dom ff by A42, Def1; hence y in dom ufs by A45; ::_thesis: verum end; A46: dom ufs = the carrier of R proof defpred S3[ set ] means ( \$1 in the carrier of R & not \$1 in dom ufs ); assume dom ufs <> the carrier of R ; ::_thesis: contradiction then consider x being set such that A47: ( ( x in dom ufs & not x in the carrier of R ) or ( x in the carrier of R & not x in dom ufs ) ) by TARSKI:1; reconsider x = x as Element of R by A29, A47; A48: S3[x] by A47; consider x0 being Element of R such that A49: S3[x0] and A50: for y being Element of R holds ( not x0 <> y or not S3[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A48, A5); set nv = x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]); set nf = ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])); A51: dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) = {x0} by FUNCOP_1:13; A52: rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= V proof ufs in PFuncs ( the carrier of R,V) by A29, A34, PARTFUN1:def_3; then ufs is PartFunc of the carrier of R,V by PARTFUN1:46; then ufs | ( the InternalRel of R -Seg x0) is PartFunc of the carrier of R,V by PARTFUN1:11; then A53: ufs | ( the InternalRel of R -Seg x0) in PFuncs ( the carrier of R,V) by PARTFUN1:45; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) or x in V ) assume A54: x in rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) ; ::_thesis: x in V assume A55: not x in V ; ::_thesis: contradiction then ( rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= (rng ufs) \/ (rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) & not x in rng ufs ) by A34, FUNCT_4:17; then A56: x in rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A54, XBOOLE_0:def_3; rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) = {(H . [x0,(ufs | ( the InternalRel of R -Seg x0))])} by FUNCOP_1:8; then x = H . (x0,(ufs | ( the InternalRel of R -Seg x0))) by A56, TARSKI:def_1; hence contradiction by A55, A53, BINOP_1:17; ::_thesis: verum end; A57: dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) = (dom ufs) \/ (dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) by FUNCT_4:def_1; dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) or x in the carrier of R ) assume that A58: x in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) and A59: not x in the carrier of R ; ::_thesis: contradiction not x in dom ufs by A29, A59; then x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A58, XBOOLE_0:def_3; hence contradiction by A51, A59; ::_thesis: verum end; then A60: ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) in PFuncs ( the carrier of R,V) by A52, PARTFUN1:def_3; x0 in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A51, TARSKI:def_1; then x0 in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) by A57, XBOOLE_0:def_3; then A61: [x0,((ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) . x0)] in ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by FUNCT_1:1; reconsider nf = ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) as PartFunc of the carrier of R,V by A60, PARTFUN1:46; A62: now__::_thesis:_for_x_being_set_st_x_in_dom_nf_holds_ nf_._x_=_H_._[x,(nf_|_(_the_InternalRel_of_R_-Seg_x))] let x be set ; ::_thesis: ( x in dom nf implies nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))] ) assume A63: x in dom nf ; ::_thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))] percases ( x in dom ufs or x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ) by A57, A63, XBOOLE_0:def_3; supposeA64: x in dom ufs ; ::_thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))] A65: {x0} misses the InternalRel of R -Seg x proof assume {x0} meets the InternalRel of R -Seg x ; ::_thesis: contradiction then consider y being set such that A66: y in {x0} and A67: y in the InternalRel of R -Seg x by XBOOLE_0:3; y = x0 by A66, TARSKI:def_1; then [x0,x] in the InternalRel of R by A67, WELLORD1:1; hence contradiction by A40, A49, A64; ::_thesis: verum end; not x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A49, A64, TARSKI:def_1; hence nf . x = ufs . x by FUNCT_4:11 .= H . [x,(ufs | ( the InternalRel of R -Seg x))] by A24, A64 .= H . [x,(nf | ( the InternalRel of R -Seg x))] by A51, A65, FUNCT_4:72 ; ::_thesis: verum end; supposeA68: x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ; ::_thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))] A69: {x0} misses the InternalRel of R -Seg x0 proof assume {x0} meets the InternalRel of R -Seg x0 ; ::_thesis: contradiction then consider x being set such that A70: x in {x0} and A71: x in the InternalRel of R -Seg x0 by XBOOLE_0:3; x = x0 by A70, TARSKI:def_1; hence contradiction by A71, WELLORD1:1; ::_thesis: verum end; A72: x = x0 by A68, TARSKI:def_1; hence nf . x = (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) . x0 by A68, FUNCT_4:13 .= H . [x0,(ufs | ( the InternalRel of R -Seg x0))] by FUNCOP_1:72 .= H . [x,(nf | ( the InternalRel of R -Seg x))] by A51, A72, A69, FUNCT_4:72 ; ::_thesis: verum end; end; end; dom nf is lower proof let x, y be set ; :: according to WELLFND1:def_1 ::_thesis: ( x in dom nf & [y,x] in the InternalRel of R implies y in dom nf ) assume that A73: x in dom nf and A74: [y,x] in the InternalRel of R ; ::_thesis: y in dom nf assume A75: not y in dom nf ; ::_thesis: contradiction then A76: not y in dom ufs by A57, XBOOLE_0:def_3; then not x in dom ufs by A40, A74; then x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A73, XBOOLE_0:def_3; then A77: x = x0 by TARSKI:def_1; reconsider y = y as Element of R by A74, ZFMISC_1:87; not y in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A75, XBOOLE_0:def_3; then y <> x0 by A51, TARSKI:def_1; hence contradiction by A50, A74, A76, A77; ::_thesis: verum end; then nf in fs by A6, A62; then [x0,(nf . x0)] in ufs by A61, TARSKI:def_4; hence contradiction by A49, FUNCT_1:1; ::_thesis: verum end; then reconsider ufs = ufs as Function of the carrier of R,V by A34, FUNCT_2:def_1, RELSET_1:4; take ufs ; ::_thesis: ufs is_recursively_expressed_by H let x be Element of the carrier of R; :: according to WELLFND1:def_5 ::_thesis: ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x))) thus ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x))) by A24, A46; ::_thesis: verum end; assume S1[] ; ::_thesis: R is well_founded then consider rk being Function of the carrier of R,(nextcard ac) such that A78: rk is_recursively_expressed_by H ; let Y be set ; :: according to WELLORD1:def_3,WELLFND1:def_2 ::_thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) ) assume that A79: Y c= the carrier of R and A80: Y <> {} ; ::_thesis: ex b1 being set st ( b1 in Y & the InternalRel of R -Seg b1 misses Y ) set m = inf (rk .: Y); consider b being set such that A81: b in Y by A80, XBOOLE_0:def_1; A82: dom rk = the carrier of R by FUNCT_2:def_1; then rk . b in rk .: Y by A79, A81, FUNCT_1:def_6; then inf (rk .: Y) in rk .: Y by ORDINAL2:17; then consider a being set such that A83: a in dom rk and A84: a in Y and A85: rk . a = inf (rk .: Y) by FUNCT_1:def_6; take a ; ::_thesis: ( a in Y & the InternalRel of R -Seg a misses Y ) thus a in Y by A84; ::_thesis: the InternalRel of R -Seg a misses Y assume ( the InternalRel of R -Seg a) /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider e being set such that A86: e in ( the InternalRel of R -Seg a) /\ Y by XBOOLE_0:def_1; A87: e in the InternalRel of R -Seg a by A86, XBOOLE_0:def_4; reconsider a = a as Element of the carrier of R by A83; reconsider rkra = rk | ( the InternalRel of R -Seg a) as Element of PFuncs ( the carrier of R,(nextcard ac)) by PARTFUN1:45; A88: rk . a = H . (a,rkra) by A78, Def5 .= sup (rng rkra) by A4 ; A89: e in Y by A86, XBOOLE_0:def_4; then reconsider rke = rk . e as Ordinal by A79, FUNCT_2:5, ORDINAL1:13; rke in rk .: Y by A82, A79, A89, FUNCT_1:def_6; then A90: inf (rk .: Y) c= rk . e by ORDINAL2:14; rke in rng rkra by A82, A79, A87, A89, FUNCT_1:50; hence contradiction by A85, A90, A88, ORDINAL1:5, ORDINAL2:19; ::_thesis: verum end; theorem :: WELLFND1:12 for R being non empty RelStr for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 ) holds R is well_founded proof let R be non empty RelStr ; ::_thesis: for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 ) holds R is well_founded let V be non trivial set ; ::_thesis: ( ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 ) implies R is well_founded ) set c = the carrier of R; set r = the InternalRel of R; set PF = PFuncs ( the carrier of R,V); set wfp = well_founded-Part R; consider a0, a1 being set such that A1: a0 in V and A2: a1 in V and A3: a0 <> a1 by ZFMISC_1:def_10; set F3 = the carrier of R --> a1; set F4 = (well_founded-Part R) --> a0; set F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0); A4: dom ( the carrier of R --> a1) = the carrier of R by FUNCOP_1:13; defpred S1[ set , Function, set ] means ( ex x being set st ( x in dom \$2 & \$2 . x = a1 ) iff \$3 = a1 ); set a01 = {a0,a1}; A5: now__::_thesis:_for_x_being_Element_of_the_carrier_of_R for_y_being_Element_of_PFuncs_(_the_carrier_of_R,V)_ex_u_being_Element_of_{a0,a1}_st_S1[x,y,u] reconsider u = a1, v = a0 as Element of {a0,a1} by TARSKI:def_2; let x be Element of the carrier of R; ::_thesis: for y being Element of PFuncs ( the carrier of R,V) ex u being Element of {a0,a1} st S1[u,b3,b4] let y be Element of PFuncs ( the carrier of R,V); ::_thesis: ex u being Element of {a0,a1} st S1[u,b2,b3] percases ( ex x being set st ( x in dom y & y . x = a1 ) or for x being set holds ( not x in dom y or not y . x = a1 ) ) ; supposeA6: ex x being set st ( x in dom y & y . x = a1 ) ; ::_thesis: ex u being Element of {a0,a1} st S1[u,b2,b3] take u = u; ::_thesis: S1[x,y,u] thus S1[x,y,u] by A6; ::_thesis: verum end; supposeA7: for x being set holds ( not x in dom y or not y . x = a1 ) ; ::_thesis: ex v being Element of {a0,a1} st S1[v,b2,b3] take v = v; ::_thesis: S1[x,y,v] thus S1[x,y,v] by A3, A7; ::_thesis: verum end; end; end; consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],{a0,a1} such that A8: for x being Element of the carrier of R for y being Element of PFuncs ( the carrier of R,V) holds S1[x,y,H . (x,y)] from BINOP_1:sch_3(A5); A9: {a0,a1} c= V by A1, A2, ZFMISC_1:32; then A10: rng H c= V by XBOOLE_1:1; (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0} \/ {a1} by XBOOLE_1:13; then A11: (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0,a1} by ENUMSET1:1; rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) by FUNCT_4:17; then rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= {a0,a1} by A11, XBOOLE_1:1; then A12: rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= V by A9, XBOOLE_1:1; A13: rng H c= {a0,a1} ; A14: dom H = [: the carrier of R,(PFuncs ( the carrier of R,V)):] by FUNCT_2:def_1; then reconsider H = H as Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V by A10, FUNCT_2:def_1, RELSET_1:4; A15: dom ((well_founded-Part R) --> a0) = well_founded-Part R by FUNCOP_1:13; A16: dom (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) = (dom ( the carrier of R --> a1)) \/ (dom ((well_founded-Part R) --> a0)) by FUNCT_4:def_1 .= the carrier of R by A4, A15, XBOOLE_1:12 ; then reconsider F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0) as Function of the carrier of R,V by A12, FUNCT_2:def_1, RELSET_1:4; A17: F2 is_recursively_expressed_by H proof let x be Element of the carrier of R; :: according to WELLFND1:def_5 ::_thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x))) reconsider F2r = F2 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45; percases ( x in well_founded-Part R or not x in well_founded-Part R ) ; supposeA18: x in well_founded-Part R ; ::_thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x))) now__::_thesis:_for_z_being_set_st_z_in_dom_F2r_holds_ F2r_._z_<>_a1 let z be set ; ::_thesis: ( z in dom F2r implies F2r . z <> a1 ) A19: the InternalRel of R -Seg x c= well_founded-Part R by A18, Th4; assume z in dom F2r ; ::_thesis: F2r . z <> a1 then A20: z in the InternalRel of R -Seg x by RELAT_1:57; then F2r . z = F2 . z by FUNCT_1:49 .= ((well_founded-Part R) --> a0) . z by A15, A20, A19, FUNCT_4:13 .= a0 by A20, A19, FUNCOP_1:7 ; hence F2r . z <> a1 by A3; ::_thesis: verum end; then A21: H . (x,F2r) <> a1 by A8; A22: H . [x,F2r] in rng H by A14, FUNCT_1:def_3; ((well_founded-Part R) --> a0) . x = a0 by A18, FUNCOP_1:7; hence F2 . x = a0 by A15, A18, FUNCT_4:13 .= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A13, A21, A22, TARSKI:def_2 ; ::_thesis: verum end; supposeA23: not x in well_founded-Part R ; ::_thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x))) then not the InternalRel of R -Seg x c= well_founded-Part R by Th9; then consider z being set such that A24: z in the InternalRel of R -Seg x and A25: not z in well_founded-Part R by TARSKI:def_3; A26: the InternalRel of R -Seg x c= the carrier of R by Th3; then A27: z in dom F2r by A16, A24, RELAT_1:57; A28: F2r . z = F2 . z by A24, FUNCT_1:49 .= ( the carrier of R --> a1) . z by A15, A25, FUNCT_4:11 .= a1 by A24, A26, FUNCOP_1:7 ; thus F2 . x = ( the carrier of R --> a1) . x by A15, A23, FUNCT_4:11 .= a1 by FUNCOP_1:7 .= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A8, A27, A28 ; ::_thesis: verum end; end; end; reconsider F1 = the carrier of R --> a0 as Function of the carrier of R,V by A1, FUNCOP_1:45; assume A29: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 ; ::_thesis: R is well_founded assume not R is well_founded ; ::_thesis: contradiction then well_founded-Part R <> the carrier of R by Th8; then consider x being set such that A30: ( ( x in well_founded-Part R & not x in the carrier of R ) or ( x in the carrier of R & not x in well_founded-Part R ) ) by TARSKI:1; A31: F1 is_recursively_expressed_by H proof let x be Element of the carrier of R; :: according to WELLFND1:def_5 ::_thesis: F1 . x = H . (x,(F1 | ( the InternalRel of R -Seg x))) reconsider F1r = F1 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45; A32: H . [x,F1r] in rng H by A14, FUNCT_1:def_3; now__::_thesis:_for_z_being_set_st_z_in_dom_F1r_holds_ F1r_._z_<>_a1 let z be set ; ::_thesis: ( z in dom F1r implies F1r . z <> a1 ) assume A33: z in dom F1r ; ::_thesis: F1r . z <> a1 then z in the InternalRel of R -Seg x by RELAT_1:57; then F1r . z = F1 . z by FUNCT_1:49 .= a0 by A33, FUNCOP_1:7 ; hence F1r . z <> a1 by A3; ::_thesis: verum end; then A34: H . (x,F1r) <> a1 by A8; thus F1 . x = a0 by FUNCOP_1:7 .= H . (x,(F1 | ( the InternalRel of R -Seg x))) by A13, A34, A32, TARSKI:def_2 ; ::_thesis: verum end; A35: F1 . x = a0 by A30, FUNCOP_1:7; F2 . x = ( the carrier of R --> a1) . x by A15, A30, FUNCT_4:11 .= a1 by A30, FUNCOP_1:7 ; hence contradiction by A3, A31, A17, A29, A35; ::_thesis: verum end; theorem :: WELLFND1:13 for R being non empty well_founded RelStr for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 proof let R be non empty well_founded RelStr ; ::_thesis: for V being non empty set for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 let V be non empty set ; ::_thesis: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 set c = the carrier of R; set r = the InternalRel of R; let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; ::_thesis: for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2 let F1, F2 be Function of the carrier of R,V; ::_thesis: ( F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H implies F1 = F2 ) assume that A1: F1 is_recursively_expressed_by H and A2: F2 is_recursively_expressed_by H ; ::_thesis: F1 = F2 defpred S1[ set ] means F1 . \$1 <> F2 . \$1; A3: dom F2 = the carrier of R by FUNCT_2:def_1; assume F1 <> F2 ; ::_thesis: contradiction then consider x being Element of the carrier of R such that A4: F1 . x <> F2 . x by FUNCT_2:63; reconsider x = x as Element of R ; A5: R is well_founded ; A6: S1[x] by A4; consider x0 being Element of R such that A7: S1[x0] and A8: for y being Element of R holds ( not x0 <> y or not S1[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch_2(A6, A5); A9: dom F1 = the carrier of R by FUNCT_2:def_1; F1 | ( the InternalRel of R -Seg x0) = F2 | ( the InternalRel of R -Seg x0) proof set fr = F1 | ( the InternalRel of R -Seg x0); set gr = F2 | ( the InternalRel of R -Seg x0); assume A10: not F1 | ( the InternalRel of R -Seg x0) = F2 | ( the InternalRel of R -Seg x0) ; ::_thesis: contradiction A11: dom (F1 | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by A9, Th3, RELAT_1:62; dom (F2 | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by A3, Th3, RELAT_1:62; then consider x1 being set such that A12: x1 in dom (F1 | ( the InternalRel of R -Seg x0)) and A13: (F1 | ( the InternalRel of R -Seg x0)) . x1 <> (F2 | ( the InternalRel of R -Seg x0)) . x1 by A11, A10, FUNCT_1:2; A14: [x1,x0] in the InternalRel of R by A11, A12, WELLORD1:1; reconsider x1 = x1 as Element of R by A12; A15: x1 <> x0 by A11, A12, WELLORD1:1; ( (F1 | ( the InternalRel of R -Seg x0)) . x1 = F1 . x1 & (F2 | ( the InternalRel of R -Seg x0)) . x1 = F2 . x1 ) by A11, A12, FUNCT_1:49; hence contradiction by A8, A13, A14, A15; ::_thesis: verum end; then F1 . x0 = H . (x0,(F2 | ( the InternalRel of R -Seg x0))) by A1, Def5 .= F2 . x0 by A2, Def5 ; hence contradiction by A7; ::_thesis: verum end; definition let R be RelStr ; let f be sequence of R; attrf is descending means :Def6: :: WELLFND1:def 6 for n being Nat holds ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ); end; :: deftheorem Def6 defines descending WELLFND1:def_6_:_ for R being RelStr for f being sequence of R holds ( f is descending iff for n being Nat holds ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) ); theorem :: WELLFND1:14 for R being non empty RelStr holds ( R is well_founded iff for f being sequence of R holds not f is descending ) proof let R be non empty RelStr ; ::_thesis: ( R is well_founded iff for f being sequence of R holds not f is descending ) set c = the carrier of R; set r = the InternalRel of R; hereby ::_thesis: ( ( for f being sequence of R holds not f is descending ) implies R is well_founded ) assume R is well_founded ; ::_thesis: for f being sequence of R holds not f is descending then A1: the InternalRel of R is_well_founded_in the carrier of R by Def2; given f being sequence of R such that A2: f is descending ; ::_thesis: contradiction A3: dom f = NAT by FUNCT_2:def_1; then rng f <> {} by RELAT_1:42; then consider a being set such that A4: a in rng f and A5: the InternalRel of R -Seg a misses rng f by A1, WELLORD1:def_3; consider n being set such that A6: n in dom f and A7: a = f . n by A4, FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by A2, Def6; then A8: f . (n + 1) in the InternalRel of R -Seg (f . n) by WELLORD1:1; f . (n + 1) in rng f by A3, FUNCT_1:def_3; hence contradiction by A5, A7, A8, XBOOLE_0:3; ::_thesis: verum end; assume A9: for f being sequence of R holds not f is descending ; ::_thesis: R is well_founded assume not R is well_founded ; ::_thesis: contradiction then not the InternalRel of R is_well_founded_in the carrier of R by Def2; then consider Y being set such that A10: Y c= the carrier of R and A11: Y <> {} and A12: for a being set holds ( not a in Y or the InternalRel of R -Seg a meets Y ) by WELLORD1:def_3; deffunc H1( set , set ) -> Element of ( the InternalRel of R -Seg \$2) /\ Y = choose (( the InternalRel of R -Seg \$2) /\ Y); consider f being Function such that A13: dom f = NAT and A14: f . 0 = choose Y and A15: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_11(); defpred S1[ Nat] means f . \$1 in Y; A16: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then the InternalRel of R -Seg (f . n) meets Y by A12; then A17: ( the InternalRel of R -Seg (f . n)) /\ Y <> {} by XBOOLE_0:def_7; f . (n + 1) = choose (( the InternalRel of R -Seg (f . n)) /\ Y) by A15; hence S1[n + 1] by A17, XBOOLE_0:def_4; ::_thesis: verum end; A18: S1[ 0 ] by A11, A14; A19: for n being Nat holds S1[n] from NAT_1:sch_2(A18, A16); rng f c= the carrier of R proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of R ) assume y in rng f ; ::_thesis: y in the carrier of R then consider x being set such that A20: x in dom f and A21: y = f . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A13, A20; f . n in Y by A19; hence y in the carrier of R by A10, A21; ::_thesis: verum end; then reconsider f = f as sequence of R by A13, FUNCT_2:2; now__::_thesis:_for_n_being_Nat_holds_ (_f_._(n_+_1)_<>_f_._n_&_[(f_._(n_+_1)),(f_._n)]_in_the_InternalRel_of_R_) let n be Nat; ::_thesis: ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) the InternalRel of R -Seg (f . n) meets Y by A12, A19; then A22: ( the InternalRel of R -Seg (f . n)) /\ Y <> {} by XBOOLE_0:def_7; f . (n + 1) = choose (( the InternalRel of R -Seg (f . n)) /\ Y) by A15; then f . (n + 1) in the InternalRel of R -Seg (f . n) by A22, XBOOLE_0:def_4; hence ( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) by WELLORD1:1; ::_thesis: verum end; then f is descending by Def6; hence contradiction by A9; ::_thesis: verum end;