Copyright (c) 1997 Association of Mizar Users
environ vocabulary PARTFUN1, FRAENKEL, FUNCT_1, RELAT_1, BOOLE, TARSKI, CARD_1, CARD_5, ORDINAL2, ORDERS_1, WELLORD1, WAYBEL_0, SETFAM_1, CAT_1, FUNCT_4, CARD_2, FINSET_1, ORDINAL1, REALSET1, FUNCOP_1, NEWTON, NORMSP_1, WELLFND1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, SETFAM_1, STRUCT_0, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, ORDINAL1, WELLORD1, ORDINAL2, FINSET_1, CARD_1, CARD_2, ORDERS_1, FRAENKEL, REALSET1, CQC_LANG, NORMSP_1, CARD_5, RFUNCT_3, WAYBEL_0; constructors NAT_1, WELLORD1, DOMAIN_1, CARD_2, REALSET1, FUNCT_4, CQC_LANG, NORMSP_1, CARD_5, RFUNCT_3, WAYBEL_0, FRAENKEL, MEMBERED; clusters SUBSET_1, STRUCT_0, RELSET_1, ORDERS_1, FRAENKEL, REALSET1, NORMSP_1, CARD_5, ALTCAT_1, WAYBEL_0, FUNCOP_1, CQC_LANG, PARTFUN1, CARD_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE; definitions TARSKI, RELAT_1, FUNCT_1, WELLORD1, WAYBEL_0, FRAENKEL, XBOOLE_0; theorems TARSKI, ENUMSET1, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, ORDINAL1, WELLORD1, GRFUNC_1, PARTFUN1, FUNCT_2, ORDINAL2, FUNCOP_1, CARD_1, ORDERS_1, FUNCT_4, FRAENKEL, CQC_LANG, NORMSP_1, CARD_4, CARD_5, SPPOL_1, AMI_5, WAYBEL_0, SETFAM_1, XBOOLE_0, XBOOLE_1; schemes NAT_1, SUBSET_1, RECDEF_1, FUNCT_2, DOMAIN_1, FUNCT_7; begin :: Preliminaries :: General preliminaries ::::::::::::::::::::::::::::::::::::::::::::: definition let A, B be set; cluster PFuncs(A,B) -> functional; coherence proof let x be set; assume x in PFuncs(A,B); then ex f being Function st x = f & dom f c= A & rng f c= B by PARTFUN1:def 5; hence x is Function; end; end; definition let R be 1-sorted, X be set, p be PartFunc of the carrier of R, X; redefine func dom p -> Subset of R; coherence proof dom p c= the carrier of R; hence thesis; end; end; theorem Th1: for X being set, f, g being Function st f c= g & X c= dom f holds f|X = g|X proof let X be set, f, g be Function; assume A1: f c= g & X c= dom f; hence f|X = g|(dom f)|X by GRFUNC_1:64 .= g|(X/\ dom f) by RELAT_1:100 .= g|X by A1,XBOOLE_1:28; end; theorem Th2: 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; assume A1: for f, g being Function st f in X & g in X holds f tolerates g; A2: union X is Relation-like proof let x be set; assume x in union X; then consider ux being set such that A3: x in ux & ux in X by TARSKI:def 4; ux is Function by A3,FRAENKEL:def 1; hence thesis by A3,RELAT_1:def 1; end; union X is Function-like proof let x,y1,y2 be set; assume A4: [x,y1] in union X & [x,y2] in union X & y1<>y2; then consider fx being set such that A5: [x, y1] in fx & fx in X by TARSKI:def 4; consider gx being set such that A6: [x, y2] in gx & gx in X by A4,TARSKI:def 4; reconsider fx, gx as Function by A5,A6,FRAENKEL:def 1; fx tolerates gx by A1,A5,A6; then consider h being Function such that A7: fx c= h & gx c= h by PARTFUN1:131; thus contradiction by A4,A5,A6,A7,FUNCT_1:def 1; end; hence union X is Function by A2; end; scheme PFSeparation {X, Y() -> set, P[set]}: ex PFS being Subset of PFuncs(X(), Y()) st for pfs being PartFunc of X(), Y() holds pfs in PFS iff P[pfs] proof defpred p[set] means P[$1]; consider fs being Subset of PFuncs (X(), Y()) such that A1: for f being set holds f in fs iff f in PFuncs(X(), Y()) & p[f] from Subset_Ex; take fs; let pfs be PartFunc of X(), Y(); pfs in PFuncs(X(), Y()) by PARTFUN1:119; hence thesis by A1; end; :: Cardinals :::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let X be set; cluster nextcard X -> non empty; coherence by CARD_1:def 6; end; definition cluster regular Aleph; existence by CARD_5:42; end; theorem Th3: for M being regular Aleph, X being set st X c= M & Card X in M holds sup X in M proof let M be regular Aleph; cf M = M by CARD_5:def 4; hence thesis by CARD_5:38; end; :: Relational structures :::::::::::::::::::::::::::::::::::::::::::::: theorem Th4: for R being RelStr, x being set holds (the InternalRel of R)-Seg x c= the carrier of R proof let R be RelStr, x be set; set r = the InternalRel of R, c = the carrier of R; r-Seg x c= field r & field r c= c \/ c by RELSET_1:19,WELLORD1:13; hence r-Seg x c= c by XBOOLE_1:1; end; definition let R be RelStr, X be Subset of R; redefine attr X is lower means :Def1: for x, y being set st x in X & [y, x] in the InternalRel of R holds y in X; compatibility proof hereby assume A1: X is lower; let x, y be set such that A2: x in X and A3: [y, x] in the InternalRel of R; x in the carrier of R & y in the carrier of R by A3,ZFMISC_1:106; then reconsider x' = x, y' = y as Element of R; y' <= x' by A3,ORDERS_1:def 9; hence y in X by A1,A2,WAYBEL_0:def 19; end; assume A4: for x, y being set st x in X & [y, x] in the InternalRel of R holds y in X; let x,y be Element of R such that A5: x in X; assume y <= x; then [y,x] in the InternalRel of R by ORDERS_1:def 9; hence thesis by A4,A5; end; end; theorem Th5: for R being RelStr, X being Subset of R, x being set st X is lower & x in X holds (the InternalRel of R)-Seg x c= X proof let R be RelStr, X be Subset of R, x be set such that A1: X is lower & x in X; let z be set; assume z in (the InternalRel of R)-Seg x; then [z,x] in (the InternalRel of R) by WELLORD1:def 1; hence z in X by A1,Def1; end; theorem Th6: for R being RelStr, X being lower Subset of R, Y being Subset of R, x being set st Y = X \/ {x} & (the InternalRel of R)-Seg x c= X holds Y is lower proof let R be RelStr, X be lower Subset of R, Y be Subset of R, x be set; set r = the InternalRel of R; assume A1: Y = X \/ {x} & r-Seg x c= X; let z, y be set; assume A2: z in Y & [y, z] in r; per cases by A1,A2,XBOOLE_0:def 2; suppose z in X; then y in X by A2,Def1; hence y in Y by A1,XBOOLE_0:def 2; suppose z in {x} & y = z; hence thesis by A2; suppose A3: z in {x} & y <> z; then z = x by TARSKI:def 1; then y in r-Seg x by A2,A3,WELLORD1:def 1; hence thesis by A1,XBOOLE_0:def 2; end; begin :: Well-founded relational structures definition let R be RelStr; attr R is well_founded means :Def2: the InternalRel of R is_well_founded_in the carrier of R; end; definition cluster non empty well_founded RelStr; existence proof reconsider er = {} as Relation of {{}} by RELSET_1:25; take R = RelStr(#{{}}, er#); thus R is non empty; let Y be set; assume Y c= the carrier of R & Y <> {}; then A1: Y = {{}} by ZFMISC_1:39; take e = {}; thus e in Y by A1,TARSKI:def 1; assume (the InternalRel of R)-Seg e /\ Y <> {}; 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 & x in Y by A2,XBOOLE_0:def 3; hence contradiction by WELLORD1:def 1; end; end; definition let R be RelStr, X be Subset of R; attr X is well_founded means :Def3: the InternalRel of R is_well_founded_in X; end; definition let R be RelStr; cluster well_founded Subset of R; existence proof {} c= the carrier of R by XBOOLE_1:2; then reconsider e = {} as Subset of R; take e; let Y be set; assume Y c= e & Y <> {}; hence thesis by XBOOLE_1:3; end; end; definition let R be RelStr; func well_founded-Part R -> Subset of R means :Def4: it = union {S where S is Subset of R : S is well_founded lower}; existence proof set IT = {S where S is Subset of R : S is well_founded lower}; IT c= bool the carrier of R proof let x be set; assume x in IT; then ex S being Subset of R st x = S & S is well_founded lower; hence x in bool the carrier of R; end; then reconsider IT as Subset-Family of R by SETFAM_1:def 7; union IT is Subset of R; hence thesis; end; uniqueness; end; definition let R be RelStr; cluster well_founded-Part R -> lower well_founded; coherence proof set wfp = well_founded-Part R, r = the InternalRel of R, IT = {S where S is Subset of R : S is well_founded lower}; A1: wfp = union IT by Def4; hereby let x, y be set; assume A2: x in wfp & [y, x] in r; then consider Y being set such that A3: x in Y & Y in IT by A1,TARSKI:def 4; consider S being Subset of R such that A4: Y = S & S is well_founded lower by A3; y in S by A2,A3,A4,Def1; hence y in wfp by A1,A3,A4,TARSKI:def 4; end; let Y be set; assume A5: Y c= wfp & Y <> {}; then consider y being set such that A6: y in Y by XBOOLE_0:def 1; consider YY being set such that A7: y in YY & YY in IT by A1,A5,A6,TARSKI:def 4; consider S being Subset of R such that A8: YY = S & S is well_founded lower by A7; A9: r is_well_founded_in S by A8,Def3; set YS = Y /\ S; YS c= S & YS <> {} by A6,A7,A8,XBOOLE_0:def 3,XBOOLE_1:17; then consider a being set such that A10: a in YS & r-Seg a misses YS by A9,WELLORD1:def 3; A11: a in Y & a in S by A10,XBOOLE_0:def 3; then r-Seg a c= S by A8,Th5; then A12: r-Seg a /\ Y = r-Seg a /\ S /\ Y by XBOOLE_1:28 .= r-Seg a /\ YS by XBOOLE_1:16; r-Seg a /\ YS = {} by A10,XBOOLE_0:def 7; then r-Seg a misses Y by A12,XBOOLE_0:def 7; hence thesis by A11; end; end; theorem Th7: for R being non empty RelStr, x be Element of R holds {x} is well_founded Subset of R proof let R be non empty RelStr, x be Element of R; set r = the InternalRel of R; reconsider sx = {x} as Subset of R; sx is well_founded proof let Y be set; assume A1: Y c= sx & Y <> {}; take x; Y = sx by A1,ZFMISC_1:39; hence x in Y by TARSKI:def 1; assume not thesis; then consider a being set such that A2: a in r-Seg x /\ Y by XBOOLE_0:4; a in r-Seg x & a in Y by A2,XBOOLE_0:def 3; then a <> x & a = x by A1,TARSKI:def 1,WELLORD1:def 1; hence contradiction; end; hence thesis; end; theorem Th8: for R being RelStr, 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, X, Y be well_founded Subset of R; set r = the InternalRel of R; assume A1: X is lower; A2: r is_well_founded_in X by Def3; A3: r is_well_founded_in Y by Def3; reconsider XY = X \/ Y as Subset of R; XY is well_founded proof let Z be set such that A4: Z c= XY & Z <> {}; set XZ = X /\ Z; A5: XZ c= X by XBOOLE_1:17; per cases; suppose XZ = {}; then X misses Z by XBOOLE_0:def 7; then Z c= Y by A4,XBOOLE_1:73; hence thesis by A3,A4,WELLORD1:def 3; suppose XZ <> {}; then consider a being set such that A6: a in XZ & r-Seg a misses XZ by A2,A5,WELLORD1:def 3; take a; thus a in Z by A6,XBOOLE_0:def 3; assume r-Seg a /\ Z <> {}; then consider b being set such that A7: b in r-Seg a /\ Z by XBOOLE_0:def 1; A8: b in r-Seg a & b in Z by A7,XBOOLE_0:def 3; then A9: b <> a & [b,a] in r by WELLORD1:def 1; a in X by A6,XBOOLE_0:def 3; then b in X by A1,A9,Def1; then b in XZ by A8,XBOOLE_0:def 3; hence contradiction by A6,A8,XBOOLE_0:3; end; hence thesis; end; theorem Th9: for R being RelStr holds R is well_founded iff well_founded-Part R = the carrier of R proof let R be RelStr; set r = the InternalRel of R, c = the carrier of R, wfp = well_founded-Part R; c c= c; then reconsider cs = c as Subset of R; set IT = {S where S is Subset of R : S is well_founded lower}; A1: wfp = union IT by Def4; hereby assume A2: R is well_founded; A3: cs is lower proof let x, y be set; thus thesis by ZFMISC_1:106; end; r is_well_founded_in cs by A2,Def2; then cs is well_founded by Def3; then cs in IT by A3; then cs c= wfp by A1,ZFMISC_1:92; hence wfp = c by XBOOLE_0:def 10; end; assume A4: wfp = c; let Y be set; assume A5: Y c= c & Y <> {}; then consider y being set such that A6: y in Y by XBOOLE_0:def 1; consider YY being set such that A7: y in YY & YY in IT by A1,A4,A5,A6,TARSKI:def 4; consider S being Subset of R such that A8: YY = S & S is well_founded lower by A7; A9: r is_well_founded_in S by A8,Def3; set YS = Y /\ S; YS c= S & YS <> {} by A6,A7,A8,XBOOLE_0:def 3,XBOOLE_1:17; then consider a being set such that A10: a in YS & r-Seg a misses YS by A9,WELLORD1:def 3; A11: r-Seg a /\ YS = {} by A10,XBOOLE_0:def 7; A12: a in Y & a in S by A10,XBOOLE_0:def 3; then r-Seg a c= S by A8,Th5; then r-Seg a /\ Y = r-Seg a /\ S /\ Y by XBOOLE_1:28 .= r-Seg a /\ YS by XBOOLE_1:16; then r-Seg a misses Y by A11,XBOOLE_0:def 7; hence thesis by A12; end; theorem Th10: for R being non empty RelStr, 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, x be Element of R; set wfp = well_founded-Part R, IT = {S where S is Subset of R : S is well_founded lower}, xwfp = wfp \/ {x}; A1: wfp = union IT by Def4; x in {x} by TARSKI:def 1; then A2: x in xwfp by XBOOLE_0:def 2; reconsider xwfp as Subset of R; assume (the InternalRel of R)-Seg x c= wfp; then A3: xwfp is lower by Th6; {x} is well_founded Subset of R by Th7; then xwfp is well_founded by Th8; then xwfp in IT by A3; hence x in wfp by A1,A2,TARSKI:def 4; end; :: Well-founded induction ::::::::::::::::::::::::::::::::::::::::::::: scheme WFMin {R() -> non empty RelStr, x() -> Element of R(), P[set]}: ex x being Element of R() st P[x] & not ex y being Element of R() st x <> y & P[y] & [y,x] in the InternalRel of R() provided A1: P[x()] and A2: R() is well_founded proof defpred p[set] means P[$1]; set c = the carrier of R(), r = the InternalRel of R(), Z = {x where x is Element of c: p[x]}; A3: Z is Subset of c from SubsetD; x() in Z by A1; then reconsider Z as non empty Subset of c by A3; r is_well_founded_in c by A2,Def2; then consider a being set such that A4: a in Z & r-Seg a misses Z by WELLORD1:def 3; reconsider a as Element of R() by A4; take a; ex a' being Element of c st a' = a & P[a'] by A4; hence P[a]; given y being Element of R() such that A5: a <> y & P[y] & [y,a] in r; y in Z & y in r-Seg a by A5,WELLORD1:def 1; hence contradiction by A4,XBOOLE_0:3; end; theorem Th11: :: WF iff WFInduction 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; set c = the carrier of R, r = the InternalRel of R; hereby assume A1: R is well_founded; let S be set such that A2: for x being Element of c st r-Seg x c= S holds x in S; assume not c c= S; then consider x being set such that A3: x in c & not x in S by TARSKI:def 3; reconsider x as Element of R by A3; defpred P[set] means $1 in c & not $1 in S; A4: P[x] by A3; consider x0 being Element of R such that A5: P[x0] and A6: not ex y being Element of R st x0 <> y & P[y] & [y,x0] in r from WFMin(A4, A1); now assume not r-Seg x0 c= S; then consider z being set such that A7: z in r-Seg x0 & not z in S by TARSKI:def 3; A8: x0 <> z & [z, x0] in r by A7,WELLORD1:def 1; then z in c by ZFMISC_1:106; then reconsider z as Element of R; z = z; hence contradiction by A6,A7,A8; end; hence contradiction by A2,A5; end; assume A9: for S being set st for x being Element of c st r-Seg x c= S holds x in S holds c c= S; assume not R is well_founded; then not r is_well_founded_in c by Def2; then consider Y being set such that A10: Y c= c & Y <> {} and A11: not ex a being set st a in Y & r-Seg a misses Y by WELLORD1:def 3; now let x be Element of c such that A12: r-Seg x c= c\Y; assume not x in c\Y; then x in Y by XBOOLE_0:def 4; then r-Seg x meets Y by A11; then consider z being set such that A13: z in r-Seg x & z in Y by XBOOLE_0:3; thus contradiction by A12,A13,XBOOLE_0:def 4; end; then c c= c\Y by A9; then Y c= c\Y by A10,XBOOLE_1:1; hence contradiction by A10,XBOOLE_1:38; end; scheme WFInduction {R() -> non empty RelStr, P[set]}: for x being Element of R() holds P[x] provided A1: for x being Element of R() st for y being Element of R() st y <> x & [y,x] in the InternalRel of R() holds P[y] holds P[x] and A2: R() is well_founded proof set c = the carrier of R(), r = the InternalRel of R(), Z = {x where x is Element of c: P[x]}; now let x be Element of c such that A3: r-Seg x c= Z; reconsider x' = x as Element of R(); now let y' be Element of R(); assume y' <> x' & [y',x'] in r; then y' in r-Seg x' by WELLORD1:def 1; then y' in Z by A3; then consider y being Element of c such that A4: y = y' & P[y]; thus P[y'] by A4; end; then P[x'] by A1; hence x in Z; end; then A5: c c= Z by A2,Th11; let x be Element of R(); x in c; then x in Z by A5; then consider x' being Element of c such that A6: x = x' & P[x']; thus thesis by A6; end; :: Well-foundedness and recursive definitions ::::::::::::::::::::::::: definition let R be non empty RelStr, V be non empty set, H be Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, F be Function; pred F is_recursively_expressed_by H means :Def5: for x being Element of R holds F.x = H.[x, F|(the InternalRel of R)-Seg x]; end; theorem :: Well foundedness and existence for R being non empty RelStr holds R is well_founded iff for V being non empty set, 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; set c = the carrier of R, r = the InternalRel of R; defpred PDR[ ] means for V being non empty set, H being Function of [:c, PFuncs(c, V):], V ex F being Function of c, V st F is_recursively_expressed_by H; thus R is well_founded implies PDR[ ] proof assume A1: R is well_founded; let V be non empty set, H be Function of [:c, PFuncs(c, V):], V; defpred P[PartFunc of c, V] means dom $1 is lower & for x being set st x in dom $1 holds $1.x = H.[x, $1 | r-Seg x]; consider fs being Subset of PFuncs(c, V) such that A2: for f being PartFunc of c, V holds f in fs iff P[f] from PFSeparation; now let f, g be Function; assume A3: f in fs & g in fs; then reconsider ff = f, gg = g as PartFunc of c,V by PARTFUN1:120; assume not f tolerates g; then consider x being set such that A4: x in dom ff /\ dom gg & ff.x <> gg.x by PARTFUN1:def 6; reconsider x as Element of R by A4; defpred P[set] means $1 in dom ff & $1 in dom gg & ff.$1 <> gg.$1; A5: P[x] by A4,XBOOLE_0:def 3; consider x0 being Element of R such that A6: P[x0] and A7: not ex y being Element of R st x0 <> y & P[y] & [y,x0] in the InternalRel of R from WFMin(A5, A1); ff | r-Seg x0 = gg | r-Seg x0 proof set fr = ff | r-Seg x0, gr = gg | r-Seg x0; assume A8: not thesis; A9: dom ff is lower by A2,A3; then r-Seg x0 c= dom ff by A6,Th5; then A10: dom fr = r-Seg x0 by RELAT_1:91; A11: dom gg is lower by A2,A3; then r-Seg x0 c= dom gg by A6,Th5; then dom fr = dom gr by A10,RELAT_1:91; then consider x1 being set such that A12: x1 in dom fr & fr.x1 <> gr.x1 by A8,FUNCT_1:9; A13: [x1, x0] in r by A10,A12,WELLORD1:def 1; reconsider x1 as Element of R by A12; A14: fr.x1 = ff.x1 & gr.x1 = gg.x1 by A10,A12,FUNCT_1:72; A15: x1 <> x0 by A10,A12,WELLORD1:def 1; x1 in dom ff & x1 in dom gg by A6,A9,A11,A13,Def1; hence contradiction by A7,A12,A13,A14,A15; end; then ff.x0 = H.[x0, gg | r-Seg x0] by A2,A3,A6 .= gg.x0 by A2,A3,A6; hence contradiction by A6; end; then reconsider ufs=union fs as Function by Th2; A16: dom ufs c= c proof let y be set; assume y in dom ufs; then [y, ufs.y] in ufs by FUNCT_1:8; then consider fx being set such that A17: [y, ufs.y] in fx & fx in fs by TARSKI:def 4; consider ff being Function such that A18: ff = fx & dom ff c= c & rng ff c= V by A17,PARTFUN1:def 5; y in dom ff by A17,A18,RELAT_1:def 4; hence y in c by A18; end; A19: rng ufs c= V proof let y be set; assume y in rng ufs; then consider x being set such that A20: x in dom ufs & y = ufs.x by FUNCT_1:def 5; [x, y] in ufs by A20,FUNCT_1:8; then consider fx being set such that A21: [x, y] in fx & fx in fs by TARSKI:def 4; consider ff being Function such that A22: ff = fx & dom ff c= c & rng ff c= V by A21,PARTFUN1:def 5; y in rng ff by A21,A22,RELAT_1:def 5; hence y in V by A22; end; A23: now let x be set; assume x in dom ufs; then [x, ufs.x] in ufs by FUNCT_1:8; then consider fx being set such that A24: [x, ufs.x] in fx & fx in fs by TARSKI:def 4; reconsider ff = fx as PartFunc of c, V by A24,PARTFUN1:120; A25: x in dom ff by A24,FUNCT_1:8; dom ff is lower by A2,A24; then A26: r-Seg x c= dom ff by A25,Th5; A27: ff c= ufs by A24,ZFMISC_1:92; thus ufs.x = ff.x by A24,FUNCT_1:8 .= H.[x, ff | r-Seg x] by A2,A24,A25 .= H.[x, ufs | r-Seg x] by A26,A27,Th1; end; A28: now let x, y be set; assume A29: x in dom ufs & [y, x] in r; then [x, ufs.x] in ufs by FUNCT_1:8; then consider fx being set such that A30: [x, ufs.x] in fx & fx in fs by TARSKI:def 4; reconsider ff = fx as PartFunc of c, V by A30,PARTFUN1:120; A31: dom ff is lower by A2,A30; x in dom ff by A30,FUNCT_1:8; then A32: y in dom ff by A29,A31,Def1; ff c= ufs by A30,ZFMISC_1:92; then dom ff c= dom ufs by GRFUNC_1:8; hence y in dom ufs by A32; end; A33: dom ufs = c proof assume dom ufs <> c; then consider x being set such that A34: not (x in dom ufs iff x in c) by TARSKI:2; reconsider x as Element of R by A16,A34; defpred P[set] means $1 in c & not $1 in dom ufs; A35: P[x] by A34; consider x0 being Element of R such that A36: P[x0] and A37: not ex y being Element of R st x0 <> y & P[y] & [y,x0] in the InternalRel of R from WFMin(A35, A1); set nv = x0 .--> H.[x0, ufs | r-Seg x0], nf = ufs +* nv; A38: dom nf = dom ufs \/ dom nv by FUNCT_4:def 1; A39: dom nv = {x0} by CQC_LANG:5; then x0 in dom nv by TARSKI:def 1; then x0 in dom nf by A38,XBOOLE_0:def 2; then A40: [x0, nf.x0] in nf by FUNCT_1:8; A41: dom nf c= c proof let x be set; assume A42: x in dom nf & not x in c; then not x in dom ufs by A16; then x in dom nv by A38,A42,XBOOLE_0:def 2; hence contradiction by A39,A42; end; rng nf c= V proof let x be set; assume A43: x in rng nf; A44: rng nf c= rng ufs \/ rng nv by FUNCT_4:18; assume A45: not x in V; then not x in rng ufs by A19; then A46: x in rng nv by A43,A44,XBOOLE_0:def 2; rng nv = {H.[x0, ufs | r-Seg x0]} by CQC_LANG:5; then A47: x = H.[x0, ufs | r-Seg x0] by A46,TARSKI:def 1; ufs in PFuncs(c, V) by A16,A19,PARTFUN1:def 5; then ufs is PartFunc of c, V by PARTFUN1:120; then ufs | r-Seg x0 is PartFunc of c, V by PARTFUN1:44; then ufs | r-Seg x0 in PFuncs(c, V) by PARTFUN1:119; hence contradiction by A45,A47,FUNCT_2:119; end; then nf in PFuncs(c, V) by A41,PARTFUN1:def 5; then reconsider nf as PartFunc of c, V by PARTFUN1:120; A48: dom nf is lower proof let x, y be set; assume A49: x in dom nf & [y,x] in r; assume A50: not y in dom nf; then A51: not y in dom ufs by A38,XBOOLE_0:def 2; then not x in dom ufs by A28,A49; then x in dom nv by A38,A49,XBOOLE_0:def 2; then A52: x = x0 by A39,TARSKI:def 1; y in the carrier of R by A49,ZFMISC_1:106; then reconsider y as Element of R; not y in dom nv by A38,A50,XBOOLE_0:def 2; then y <> x0 by A39,TARSKI:def 1; hence contradiction by A37,A49,A51,A52; end; now let x be set; assume A53: x in dom nf; per cases by A38,A53,XBOOLE_0:def 2; suppose A54: x in dom ufs; then A55: not x in dom nv by A36,A39,TARSKI:def 1; A56: {x0} misses r-Seg x proof assume {x0} meets r-Seg x; then consider y being set such that A57: y in {x0} & y in r-Seg x by XBOOLE_0:3; y = x0 by A57,TARSKI:def 1; then [x0, x] in r by A57,WELLORD1:def 1; hence contradiction by A28,A36,A54; end; thus nf.x = ufs.x by A55,FUNCT_4:12 .= H.[x, ufs | r-Seg x] by A23,A54 .= H.[x, nf | r-Seg x] by A39,A56,AMI_5:7; suppose A58: x in dom nv; then A59: x = x0 by A39,TARSKI:def 1; A60: {x0} misses r-Seg x0 proof assume {x0} meets r-Seg x0; then consider x being set such that A61: x in {x0} & x in r-Seg x0 by XBOOLE_0:3; x = x0 by A61,TARSKI:def 1; hence contradiction by A61,WELLORD1:def 1; end; thus nf.x = nv.x0 by A58,A59,FUNCT_4:14 .= H.[x0, ufs | r-Seg x0] by CQC_LANG:6 .= H.[x, nf | r-Seg x] by A39,A59,A60,AMI_5:7; end; then nf in fs by A2,A48; then [x0, nf.x0] in ufs by A40,TARSKI:def 4; hence contradiction by A36,FUNCT_1:8; end; then reconsider ufs as Function of c, V by A19,FUNCT_2:def 1,RELSET_1:11; take ufs; let x be Element of c; thus thesis by A23,A33; end; assume A62: PDR[ ]; reconsider ac = alef 0 +` Card c as infinite Cardinal; set V = nextcard ac; deffunc F(Element of c, Element of PFuncs(c, V)) = sup rng $2; A63: for x being Element of c, p being Element of PFuncs(c, V) holds F(x,p) in V proof let x be Element of c, p be Element of PFuncs(c, V); Card dom p c= Card c & Card rng p c= Card dom p by CARD_1:27,28; then A64: Card rng p c= Card c by XBOOLE_1:1; Card c c= ac by CARD_4:72; then A65: Card rng p c= ac by A64,XBOOLE_1:1; ac in V by CARD_1:32; then A66: Card rng p in V by A65,ORDINAL1:22; V is regular by CARD_5:42; hence sup rng p in V by A66,Th3; end; consider H being Function of [:c, PFuncs(c, V):], V such that A67: for x being Element of c, p being Element of PFuncs(c, V) holds H.[x,p] = F(x,p) from Kappa2D(A63); consider rk being Function of c, V such that A68: rk is_recursively_expressed_by H by A62; A69: dom rk = c by FUNCT_2:def 1; let Y be set; assume A70: Y c= c & Y <> {}; then consider b being set such that A71: b in Y by XBOOLE_0:def 1; set m = inf (rk.:Y); rk.b in V by A70,A71,FUNCT_2:7; then rk.b in rk.:Y & rk.b is Ordinal by A69,A70,A71,FUNCT_1:def 12,ORDINAL1:23; then m in rk.:Y by ORDINAL2:25; then consider a being set such that A72: a in dom rk & a in Y & rk.a = m by FUNCT_1:def 12; take a; thus a in Y by A72; assume r-Seg(a) /\ Y <> {}; then consider e being set such that A73: e in r-Seg(a) /\ Y by XBOOLE_0:def 1; A74: e in r-Seg a & e in Y by A73,XBOOLE_0:def 3; then rk.e in V by A70,FUNCT_2:7; then reconsider rke = rk.e as Ordinal by ORDINAL1:23; rke in rk.:Y by A69,A70,A74,FUNCT_1:def 12; then A75: m c= rk.e by ORDINAL2:22; reconsider a as Element of c by A72; reconsider rkra = rk | r-Seg a as Element of PFuncs(c,V) by PARTFUN1:119; A76: rk.a = H.[a, rkra] by A68,Def5 .= sup rng rkra by A67; rke in rng rkra by A69,A70,A74,FUNCT_1:73; then rk.e in m by A72,A76,ORDINAL2:27; hence contradiction by A75,ORDINAL1:7; end; theorem :: Uniqueness implies well-foundedness for R being non empty RelStr, V being non trivial set st for H being Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, 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, V be non trivial set; set c = the carrier of R, r = the InternalRel of R, PF = PFuncs(c, V), wfp = well_founded-Part R; consider a0, a1 being set such that A1: a0 in V & a1 in V & a0 <> a1 by SPPOL_1:3; set a01 = {a0, a1}; A2: a01 c= V by A1,ZFMISC_1:38; set F3 = c --> a1, F4 = wfp --> a0, F2 = F3 +* F4; A3: dom F3 = c by FUNCOP_1:19; A4: dom F4 = wfp by FUNCOP_1:19; A5: dom F2 = dom F3 \/ dom F4 by FUNCT_4:def 1 .= c by A3,A4,XBOOLE_1:12; reconsider F1 = c --> a0 as Function of c, V by A1,FUNCOP_1:57; rng F3 c= {a1} & rng F4 c= {a0} by FUNCOP_1:19; then rng F3 \/ rng F4 c= {a0} \/ {a1} by XBOOLE_1:13; then rng F3 \/ rng F4 c= a01 & rng F2 c= rng F3 \/ rng F4 by ENUMSET1:41,FUNCT_4:18; then rng F2 c= a01 by XBOOLE_1:1; then rng F2 c= V by A2,XBOOLE_1:1; then reconsider F2 as Function of c, V by A5,FUNCT_2:def 1,RELSET_1:11; defpred P[set,Function,set] means (ex x being set st x in dom $2 & $2.x = a1) iff $3 = a1; A6: now let x be Element of c, y be Element of PF; reconsider u = a1, v = a0 as Element of a01 by TARSKI:def 2; per cases; suppose A7: ex x being set st x in dom y & y.x = a1; take u; thus P[x,y,u] by A7; suppose A8: not ex x being set st x in dom y & y.x = a1; take v; thus P[x,y,v] by A1,A8; end; consider H being Function of [:c, PF:], a01 such that A9: for x being Element of c, y being Element of PF holds P[x,y,H.[x,y]] from FuncEx2D(A6); A10: rng H c= a01; A11: dom H = [:c, PF:] & rng H c= V by A2,FUNCT_2:def 1,XBOOLE_1:1; then reconsider H as Function of [:c, PF:], V by FUNCT_2:def 1,RELSET_1:11; A12: F1 is_recursively_expressed_by H proof let x be Element of c; reconsider F1r = F1 | r-Seg x as Element of PF by PARTFUN1:119; now let z be set; assume A13: z in dom F1r; then z in r-Seg x & z in dom F1 by RELAT_1:86; then F1r.z = F1.z by FUNCT_1:72 .= a0 by A13,FUNCOP_1:13; hence F1r.z <> a1 by A1; end; then A14: H.[x, F1r] <> a1 by A9; [x, F1r] in dom H by A11,ZFMISC_1:106; then A15: H.[x, F1r] in rng H by FUNCT_1:def 5; thus F1.x = a0 by FUNCOP_1:13 .= H.[x, F1 | r-Seg x] by A10,A14,A15,TARSKI:def 2; end; A16: F2 is_recursively_expressed_by H proof let x be Element of c; reconsider F2r = F2 | r-Seg x as Element of PF by PARTFUN1:119; per cases; suppose A17: x in wfp; now let z be set; assume z in dom F2r; then A18: z in r-Seg x & z in dom F2 by RELAT_1:86; A19: r-Seg x c= wfp by A17,Th5; F2r.z = F2.z by A18,FUNCT_1:72 .= F4.z by A4,A18,A19,FUNCT_4:14 .= a0 by A18,A19,FUNCOP_1:13; hence F2r.z <> a1 by A1; end; then A20: H.[x, F2r]<>a1 by A9; [x, F2r] in dom H by A11,ZFMISC_1:106; then A21: H.[x, F2r] in rng H by FUNCT_1:def 5; F4.x = a0 by A17, FUNCOP_1:13; hence F2.x = a0 by A4,A17,FUNCT_4:14 .= H.[x, F2 | r-Seg x] by A10,A20,A21,TARSKI:def 2; suppose A22: not x in wfp; then not r-Seg x c= wfp by Th10; then consider z being set such that A23: z in r-Seg x & not z in wfp by TARSKI:def 3; A24: r-Seg x c= c by Th4; then A25: z in dom F2r by A5,A23,RELAT_1:86; A26: F2r.z = F2.z by A23,FUNCT_1:72 .= F3.z by A4,A23,FUNCT_4:12 .= a1 by A23,A24,FUNCOP_1:13; thus F2.x = F3.x by A4,A22,FUNCT_4:12 .= a1 by FUNCOP_1:13 .= H.[x, F2 | r-Seg x] by A9,A25,A26; end; assume A27: for H being Function of [:c, PF:], V, F1, F2 being Function of c, V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds F1 = F2; assume not R is well_founded; then wfp <> c by Th9; then consider x being set such that A28: not (x in wfp iff x in c) by TARSKI:2; A29: F1.x = a0 by A28,FUNCOP_1:13; F2.x = F3.x by A4,A28,FUNCT_4:12 .= a1 by A28,FUNCOP_1:13; hence contradiction by A1,A12,A16,A27,A29; end; theorem :: Well-foundedness implies uniqueness for R being non empty well_founded RelStr, V being non empty set, H being Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, 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, V be non empty set; set c = the carrier of R, r = the InternalRel of R; let H be Function of [:c, PFuncs(c, V):], V, F1, F2 be Function of c, V; assume that A1: F1 is_recursively_expressed_by H and A2: F2 is_recursively_expressed_by H; A3: dom F1 = c & dom F2 = c by FUNCT_2:def 1; assume F1 <> F2; then consider x being Element of c such that A4: F1.x <> F2.x by FUNCT_2:113; reconsider x as Element of R; defpred P[set] means F1.$1 <> F2.$1; A5: P[x] by A4; A6: R is well_founded; consider x0 being Element of R such that A7: P[x0] and A8: not ex y being Element of R st x0 <> y & P[y] & [y,x0] in r from WFMin(A5, A6); F1 | r-Seg x0 = F2 | r-Seg x0 proof set fr = F1 | r-Seg x0, gr = F2 | r-Seg x0; r-Seg x0 c= c by Th4; then A9: dom fr = r-Seg x0 & dom gr = r-Seg x0 by A3,RELAT_1:91; assume not thesis; then consider x1 being set such that A10: x1 in dom fr & fr.x1 <> gr.x1 by A9,FUNCT_1:9; A11: [x1, x0] in r by A9,A10,WELLORD1:def 1; reconsider x1 as Element of R by A10; A12: fr.x1 = F1.x1 & gr.x1 = F2.x1 by A9,A10,FUNCT_1:72; x1 <> x0 by A9,A10,WELLORD1:def 1; hence contradiction by A8,A10,A11,A12; end; then F1.x0 = H.[x0, F2 | r-Seg x0] by A1,Def5 .= F2.x0 by A2,Def5; hence contradiction by A7; end; :: Well-foundedness and omega chains ::::::::::::::::::::::::::::::::: definition let R be RelStr, f be sequence of R; canceled; attr f is descending means :Def7: for n being Nat holds f.(n+1) <> f.n & [f.(n+1), f.n] in the InternalRel of R; end; theorem :: omega chains for R being non empty RelStr holds R is well_founded iff not ex f being sequence of R st f is descending proof let R be non empty RelStr; set c = the carrier of R, r = the InternalRel of R; hereby assume R is well_founded; then A1: r is_well_founded_in c by Def2; given f being sequence of R such that A2: f is descending; A3: dom f = NAT & rng f c= c by FUNCT_2:def 1; then rng f <> {} by RELAT_1:65; then consider a being set such that A4: a in rng f & r-Seg(a) misses rng f by A1,WELLORD1:def 3; consider n being set such that A5: n in dom f & a = f.n by A4,FUNCT_1:def 5; reconsider n as Nat by A5; f.(n+1)<>f.n & [f.(n+1),f.n] in the InternalRel of R by A2,Def7; then A6: f.(n+1) in r-Seg(f.n) by WELLORD1:def 1; f.(n+1) in rng f by A3,FUNCT_1:def 5; hence contradiction by A4,A5,A6,XBOOLE_0:3; end; assume A7: not ex f being sequence of R st f is descending; assume not R is well_founded; then not r is_well_founded_in c by Def2; then consider Y being set such that A8: Y c= c & Y <> {} and A9: for a being set holds not a in Y or r-Seg(a) meets Y by WELLORD1:def 3; deffunc G(set,set) = choose (r-Seg($2) /\ Y); consider f being Function such that A10: dom f = NAT and A11: f.0 = choose Y and A12: for n being Element of NAT holds f.(n+1) = G(n,f.n) from LambdaRecEx; defpred P[Nat] means f.$1 in Y; A13: P[0] by A8,A11; A14: now let n be Nat; assume P[n]; then r-Seg(f.n) meets Y by A9; then A15: r-Seg(f.n) /\ Y <> {} by XBOOLE_0:def 7; f.(n+1) = choose (r-Seg(f.n) /\ Y) by A12; hence P[n+1] by A15,XBOOLE_0:def 3; end; A16: for n being Nat holds P[n] from Ind(A13, A14); rng f c= c proof let y be set; assume y in rng f; then consider x being set such that A17: x in dom f & y = f.x by FUNCT_1:def 5; reconsider n = x as Nat by A10,A17; f.n in Y by A16; hence y in c by A8,A17; end; then f is Function of NAT, c by A10,FUNCT_2:4; then reconsider f as sequence of R by NORMSP_1:def 3; now let n be Nat; f.n in Y by A16; then r-Seg(f.n) meets Y by A9; then A18: r-Seg(f.n) /\ Y <> {} by XBOOLE_0:def 7; f.(n+1) = choose (r-Seg(f.n) /\ Y) by A12; then f.(n+1) in r-Seg(f.n) by A18,XBOOLE_0:def 3; hence f.(n+1) <> f.n & [f.(n+1), f.n] in r by WELLORD1:def 1; end; then f is descending by Def7; hence contradiction by A7; end;