### The Mizar article:

### Boolean Posets, Posets under Inclusion and Products of Relational Structures

**by****Adam Grabowski, and****Robert Milewski**

- Received September 20, 1996
Copyright (c) 1996 Association of Mizar Users

- MML identifier: YELLOW_1
- [ MML identifier index ]

environ vocabulary LATTICES, LATTICE3, ORDERS_1, FILTER_1, BOOLE, BHSP_3, WELLORD2, RELAT_1, RELAT_2, CAT_1, YELLOW_0, WELLORD1, TARSKI, SETFAM_1, ORDINAL2, PRE_TOPC, REALSET1, PRALG_1, FUNCT_1, PBOOLE, FUNCOP_1, CARD_3, RLVECT_2, GROUP_1, FUNCT_2, SEQM_3, ORDERS_3, YELLOW_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, REALSET1, FUNCT_1, STRUCT_0, TOPS_2, WELLORD2, TOLER_1, PARTFUN1, FUNCT_2, ORDERS_1, LATTICES, ORDERS_3, LATTICE3, PRE_TOPC, PRE_CIRC, PBOOLE, CARD_3, PRALG_1, YELLOW_0; constructors YELLOW_0, WELLORD2, TOLER_1, ORDERS_3, TOPS_2, PRE_CIRC, KNASTER; clusters STRUCT_0, LATTICES, LATTICE3, YELLOW_0, ORDERS_1, RELSET_1, CANTOR_1, PRE_TOPC, KNASTER, FUNCOP_1, SUBSET_1, PARTFUN1, XBOOLE_0; requirements SUBSET, BOOLE; definitions LATTICE3, XBOOLE_0, TOPS_2, TARSKI, RELAT_1, PRALG_1; theorems REALSET1, TARSKI, LATTICES, LATTICE3, YELLOW_0, STRUCT_0, RELAT_1, ORDERS_1, RELAT_2, RELSET_1, ZFMISC_1, WELLORD2, SETFAM_1, PRE_TOPC, TOPS_2, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, FUNCT_2, PRALG_1, FUNCT_4, ORDERS_3, XBOOLE_0, XBOOLE_1, PARTFUN1; schemes RELSET_1, FUNCT_2; begin :: Boolean Posets and Posets under Inclusion reserve X for set; definition let L be Lattice; cluster LattPOSet L -> with_suprema with_infima; coherence by LATTICE3:11; end; definition let L be upper-bounded Lattice; cluster LattPOSet L -> upper-bounded; coherence proof ex x being Element of LattPOSet L st x is_>=_than the carrier of LattPOSet L proof A1: the carrier of LattPOSet L = the carrier of RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2 .= the carrier of L; consider z be Element of L such that A2: for v being Element of L holds z"\/"v = z & v"\/"z = z by LATTICES:def 14; reconsider z' = z as Element of LattPOSet L by A1; A3: z' is_<=_than {} by YELLOW_0:6; A4: z = Top L by A2,LATTICES:def 17; now let b' be Element of LattPOSet L; reconsider b = b' as Element of L by A1; assume b' is_<=_than {}; A5: b% = b & z% = z by LATTICE3:def 3; b [= z by A4,LATTICES:45; hence z' >= b' by A5,LATTICE3:7; end; then A6: z' = "/\"({},LattPOSet L) by A3,YELLOW_0:31; take x = Top (LattPOSet L); now let a be Element of LattPOSet L; assume a in the carrier of LattPOSet L; reconsider a' = a as Element of L by A1; reconsider x' = x as Element of L by A1; A7: a'% = a' & x'% = x' by LATTICE3:def 3; Top (LattPOSet L) = Top L by A4,A6,YELLOW_0:def 12; then a' [= x' by LATTICES:45; hence a <= x by A7,LATTICE3:7; end; hence x is_>=_than the carrier of LattPOSet L by LATTICE3:def 9; end; hence LattPOSet L is upper-bounded by YELLOW_0:def 5; end; end; definition let L be lower-bounded Lattice; cluster LattPOSet L -> lower-bounded; coherence proof ex x being Element of LattPOSet L st x is_<=_than the carrier of LattPOSet L proof A1: the carrier of LattPOSet L = the carrier of RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2 .= the carrier of L; consider z be Element of L such that A2: for v being Element of L holds z"/\"v = z & v"/\"z = z by LATTICES:def 13; reconsider z' = z as Element of LattPOSet L by A1; A3: z' is_>=_than {} by YELLOW_0:6; A4: z = Bottom L by A2,LATTICES:def 16; now let b' be Element of LattPOSet L; reconsider b = b' as Element of L by A1; assume b' is_>=_than {}; A5: b% = b & z% = z by LATTICE3:def 3; z [= b by A4,LATTICES:41; hence z' <= b' by A5,LATTICE3:7; end; then A6: z' = "\/"({},LattPOSet L) by A3,YELLOW_0:30; take x = Bottom (LattPOSet L); now let a be Element of LattPOSet L; assume a in the carrier of LattPOSet L; reconsider a' = a as Element of L by A1; reconsider x' = x as Element of L by A1; A7: a'% = a' & x'% = x' by LATTICE3:def 3; Bottom (LattPOSet L) = Bottom L by A4,A6,YELLOW_0:def 11; then x' [= a' by LATTICES:41; hence x <= a by A7,LATTICE3:7; end; hence x is_<=_than the carrier of LattPOSet L by LATTICE3:def 8; end; hence LattPOSet L is lower-bounded by YELLOW_0:def 4; end; end; definition let L be complete Lattice; cluster LattPOSet L -> complete; coherence proof for X be set ex a be Element of LattPOSet L st X is_<=_than a & for b being Element of LattPOSet L st X is_<=_than b holds a <= b proof A1: the carrier of LattPOSet L = the carrier of RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2 .= the carrier of L; let X be set; take a = "\/"(X,LattPOSet L); A2: a = "\/"(X,L) by YELLOW_0:29; X is_less_than "\/"(X,L) by LATTICE3:def 21; then X is_<=_than "\/"(X,L)% by LATTICE3:30; hence X is_<=_than a by A2,LATTICE3:def 3; let b be Element of LattPOSet L; reconsider b' = b as Element of L by A1; A3: "\/"(X,L)% = a & b'% = b by A2,LATTICE3:def 3; assume X is_<=_than b; then X is_<=_than b'% by LATTICE3:def 3; then X is_less_than b' by LATTICE3:30; then "\/"(X,L) [= b' by LATTICE3:def 21; hence a <= b by A3,LATTICE3:7; end; hence thesis by LATTICE3:def 12; end; end; definition let X be set; redefine func RelIncl X -> Order of X; coherence proof now let x be set; assume A1: x in RelIncl X; then consider y,z be set such that A2: x = [y,z] by RELAT_1:def 1; y in field RelIncl X & z in field RelIncl X by A1,A2,RELAT_1:30; then y in X & z in X by WELLORD2:def 1; hence x in [:X,X:] by A2,ZFMISC_1:106; end; then RelIncl X c= [:X,X:] by TARSKI:def 3; then reconsider R = RelIncl X as Relation of X by RELSET_1:def 1; A3: field R = X by WELLORD2:def 1; R is reflexive by WELLORD2:2; then A4: R is_reflexive_in X by A3,RELAT_2:def 9; A5: R is antisymmetric by WELLORD2:5; A6: R is transitive by WELLORD2:3; dom R = X by A4,ORDERS_1:98; hence thesis by A5,A6,PARTFUN1:def 4,WELLORD2:2; end; end; definition let X be set; func InclPoset X -> strict RelStr equals :Def1: RelStr(#X, RelIncl X#); correctness; end; definition let X be set; cluster InclPoset X -> reflexive antisymmetric transitive; coherence proof InclPoset X = RelStr(#X, RelIncl X#) by Def1; hence thesis; end; end; definition let X be non empty set; cluster InclPoset X -> non empty; coherence proof InclPoset X = RelStr(#X, RelIncl X#) by Def1; hence thesis; end; end; theorem Th1: the carrier of InclPoset X = X & the InternalRel of InclPoset X = RelIncl X proof InclPoset X = RelStr (#X, RelIncl X#) by Def1; hence thesis; end; definition let X be set; func BoolePoset X -> strict RelStr equals :Def2: LattPOSet BooleLatt X; correctness; end; definition let X be set; cluster BoolePoset X -> non empty reflexive antisymmetric transitive; coherence proof BoolePoset X = LattPOSet BooleLatt X by Def2; hence thesis; end; end; definition let X be set; cluster BoolePoset X -> complete; coherence proof BoolePoset X = LattPOSet BooleLatt X by Def2; hence thesis; end; end; theorem Th2: for x,y be Element of BoolePoset X holds x <= y iff x c= y proof let x,y be Element of BoolePoset X; set B = BoolePoset X, L = BooleLatt X; the carrier of LattPOSet L = the carrier of L proof LattPOSet BooleLatt X = RelStr (#the carrier of L, LattRel L#) by LATTICE3:def 2; hence thesis; end; then reconsider x' = x, y' = y as Element of BooleLatt X by Def2; A1: the InternalRel of B = the InternalRel of LattPOSet L by Def2; A2: x'% = x & y'% = y by LATTICE3:def 3; thus x <= y implies x c= y proof assume x <= y; then [x,y] in the InternalRel of B by ORDERS_1:def 9; then x'% <= y'% by A1,A2,ORDERS_1:def 9; then x' [= y' by LATTICE3:7; hence x c= y by LATTICE3:2; end; thus x c= y implies x <= y proof assume x c= y; then x' [= y' by LATTICE3:2; then x'% <= y'% by LATTICE3:7; hence x <= y by A2,Def2; end; end; theorem Th3: for X be non empty set, x,y be Element of InclPoset X holds x <= y iff x c= y proof let X be non empty set; let x,y be Element of InclPoset X; x in the carrier of InclPoset X & y in the carrier of InclPoset X; then A1: x in X & y in X by Th1; thus x <= y implies x c= y proof assume x <= y; then [x,y] in the InternalRel of InclPoset X by ORDERS_1:def 9; then [x,y] in RelIncl X by Th1; hence x c= y by A1,WELLORD2:def 1; end; thus x c= y implies x <= y proof assume x c= y; then [x,y] in RelIncl X by A1,WELLORD2:def 1; then [x,y] in the InternalRel of InclPoset X by Th1; hence x <= y by ORDERS_1:def 9; end; end; theorem Th4: BoolePoset X = InclPoset bool X proof set B = BoolePoset X; A1: the carrier of B = the carrier of LattPOSet BooleLatt X by Def2 .= the carrier of RelStr(#the carrier of BooleLatt X, LattRel BooleLatt X#) by LATTICE3:def 2 .= bool X by LATTICE3:def 1; then reconsider In = the InternalRel of B as Relation of bool X; for x be set st x in bool X ex y be set st [x,y] in In proof let x be set; assume x in bool X; then reconsider x' = x as Element of B by A1; take y = x'; x' <= y; hence [x,y] in In by ORDERS_1:def 9; end; then A2: dom In = bool X by RELSET_1:22; for y be set st y in bool X ex x be set st [x,y] in In proof let y be set; assume y in bool X; then reconsider y' = y as Element of B by A1; take x = y'; x <= y'; hence [x,y] in In by ORDERS_1:def 9; end; then rng In = bool X by RELSET_1:23; then A3: field the InternalRel of B = bool X \/ bool X by A2,RELAT_1:def 6; now let Y,Z be set; assume Y in bool X & Z in bool X; then reconsider Y' = Y , Z' = Z as Element of B by A1; thus [Y,Z] in the InternalRel of B implies Y c= Z proof assume [Y,Z] in the InternalRel of B; then Y' <= Z' by ORDERS_1:def 9; hence Y c= Z by Th2; end; thus Y c= Z implies [Y,Z] in the InternalRel of B proof assume Y c= Z; then Y' <= Z' by Th2; hence [Y,Z] in the InternalRel of B by ORDERS_1:def 9; end; end; then A4:the InternalRel of B = RelIncl bool X by A3,WELLORD2:def 1; the carrier of B = the carrier of InclPoset bool X by A1,Th1; hence thesis by A4,Th1; end; theorem for Y be Subset of bool X holds InclPoset Y is full SubRelStr of BoolePoset X proof set L = BoolePoset X; let Y be Subset of bool X; A1: the carrier of L = the carrier of LattPOSet BooleLatt X by Def2 .= the carrier of RelStr(#the carrier of BooleLatt X, LattRel BooleLatt X#) by LATTICE3:def 2 .= bool X by LATTICE3:def 1; then reconsider Y' = Y as Subset of L; reconsider In = the InternalRel of L as Relation of bool X by A1; for x be set st x in bool X ex y be set st [x,y] in In proof let x be set; assume x in bool X; then reconsider x' = x as Element of L by A1; take y = x'; x' <= y; hence [x,y] in In by ORDERS_1:def 9; end; then A2: dom In = bool X by RELSET_1:22; for y be set st y in bool X ex x be set st [x,y] in In proof let y be set; assume y in bool X; then reconsider y' = y as Element of L by A1; take x = y'; x <= y'; hence [x,y] in In by ORDERS_1:def 9; end; then rng In = bool X by RELSET_1:23; then A3: field the InternalRel of L = bool X \/ bool X by A2,RELAT_1:def 6; now let Y,Z be set; assume Y in bool X & Z in bool X; then reconsider Y' = Y , Z' = Z as Element of L by A1; thus [Y,Z] in the InternalRel of L implies Y c= Z proof assume [Y,Z] in the InternalRel of L; then Y' <= Z' by ORDERS_1:def 9; hence Y c= Z by Th2; end; thus Y c= Z implies [Y,Z] in the InternalRel of L proof assume Y c= Z; then Y' <= Z' by Th2; hence [Y,Z] in the InternalRel of L by ORDERS_1:def 9; end; end; then A4: the InternalRel of L = RelIncl bool X by A3,WELLORD2:def 1; RelStr(#Y',(the InternalRel of L) |_2 Y'#) is full SubRelStr of L by YELLOW_0:57; then RelStr(#Y',RelIncl Y'#) is full SubRelStr of L by A4,WELLORD2:8; hence InclPoset Y is full SubRelStr of L by Def1; end; theorem for X be non empty set holds InclPoset X is with_suprema implies for x,y be Element of InclPoset X holds x \/ y c= x "\/" y proof let X be non empty set; assume A1: InclPoset X is with_suprema; let x,y be Element of InclPoset X; x <= x "\/" y & y <= x "\/" y by A1,YELLOW_0:22; then x c= x "\/" y & y c= x "\/" y by Th3; hence x \/ y c= x "\/" y by XBOOLE_1:8; end; theorem for X be non empty set holds InclPoset X is with_infima implies for x,y be Element of InclPoset X holds x "/\" y c= x /\ y proof let X be non empty set; assume A1: InclPoset X is with_infima; let x,y be Element of InclPoset X; x "/\" y <= x & x "/\" y <= y by A1,YELLOW_0:23; then x "/\" y c= x & x "/\" y c= y by Th3; hence x "/\" y c= x /\ y by XBOOLE_1:19; end; theorem Th8: for X be non empty set holds for x,y be Element of InclPoset X st x \/ y in X holds x "\/" y = x \/ y proof let X be non empty set; let x,y be Element of InclPoset X; assume x \/ y in X; then x \/ y in the carrier of InclPoset X by Th1; then reconsider z = x \/ y as Element of InclPoset X; x c= z & y c= z by XBOOLE_1:7; then A1: x <= z & y <= z by Th3; now let c be Element of InclPoset X; assume x <= c & y <= c; then x c= c & y c= c by Th3; then z c= c by XBOOLE_1:8; hence z <= c by Th3; end; hence thesis by A1,LATTICE3:def 13; end; theorem Th9: for X be non empty set for x,y be Element of InclPoset X st x /\ y in X holds x "/\" y = x /\ y proof let X be non empty set; let x,y be Element of InclPoset X; assume x /\ y in X; then x /\ y in the carrier of InclPoset X by Th1; then reconsider z = x /\ y as Element of InclPoset X; z c= x & z c= y by XBOOLE_1:17; then A1: z <= x & z <= y by Th3; now let c be Element of InclPoset X; assume c <= x & c <= y; then c c= x & c c= y by Th3; then c c= z by XBOOLE_1:19; hence c <= z by Th3; end; hence thesis by A1,LATTICE3:def 14; end; theorem for L be RelStr st for x,y be Element of L holds x <= y iff x c= y holds the InternalRel of L = RelIncl the carrier of L proof let L be RelStr; assume A1: for x,y be Element of L holds x <= y iff x c= y; for x be set st x in the carrier of L ex y be set st [x,y] in the InternalRel of L proof let x be set; assume x in the carrier of L; then reconsider x' = x as Element of L; take y = x'; x' <= y by A1; hence [x,y] in the InternalRel of L by ORDERS_1:def 9; end; then A2: dom the InternalRel of L = the carrier of L by RELSET_1:22; for y be set st y in the carrier of L ex x be set st [x,y] in the InternalRel of L proof let y be set; assume y in the carrier of L; then reconsider y' = y as Element of L; take x = y'; x <= y' by A1; hence [x,y] in the InternalRel of L by ORDERS_1:def 9; end; then rng the InternalRel of L = the carrier of L by RELSET_1:23; then A3: field the InternalRel of L = (the carrier of L) \/ the carrier of L by A2,RELAT_1:def 6; now let Y,Z be set; assume Y in the carrier of L & Z in the carrier of L; then reconsider Y' = Y , Z' = Z as Element of L; thus [Y,Z] in the InternalRel of L implies Y c= Z proof assume [Y,Z] in the InternalRel of L; then Y' <= Z' by ORDERS_1:def 9; hence Y c= Z by A1; end; thus Y c= Z implies [Y,Z] in the InternalRel of L proof assume Y c= Z; then Y' <= Z' by A1; hence [Y,Z] in the InternalRel of L by ORDERS_1:def 9; end; end; hence the InternalRel of L = RelIncl the carrier of L by A3,WELLORD2:def 1; end; theorem for X be non empty set st (for x,y be set st (x in X & y in X) holds x \/ y in X) holds InclPoset X is with_suprema proof let X be non empty set; set L = InclPoset X; assume A1: for x,y be set st (x in X & y in X) holds x \/ y in X; now let a,b be Element of L; a in the carrier of L & b in the carrier of L; then a in X & b in X by Th1; then A2: a \/ b in X by A1; ex c be Element of L st {a,b} is_<=_than c & for d be Element of L st {a,b} is_<=_than d holds c <= d proof take c = a "\/" b; a \/ b = c by A2,Th8; then a c= c & b c= c by XBOOLE_1:7; then a <= c & b <= c by Th3; hence {a,b} is_<=_than c by YELLOW_0:8; let d be Element of L; assume A3: {a,b} is_<=_than d; a in {a,b} by TARSKI:def 2; then A4: a <= d by A3,LATTICE3:def 9; b in {a,b} by TARSKI:def 2; then b <= d by A3,LATTICE3:def 9; then a c= d & b c= d by A4,Th3; then a \/ b c= d by XBOOLE_1:8; then c c= d by A2,Th8; hence c <= d by Th3; end; hence ex_sup_of {a,b}, L by YELLOW_0:15; end; hence L is with_suprema by YELLOW_0:20; end; theorem for X be non empty set st for x,y be set st (x in X & y in X) holds x /\ y in X holds InclPoset X is with_infima proof let X be non empty set; set L = InclPoset X; assume A1: for x,y be set st (x in X & y in X) holds x /\ y in X; now let a,b be Element of L; a in the carrier of L & b in the carrier of L; then a in X & b in X by Th1; then A2: a /\ b in X by A1; ex c be Element of L st {a,b} is_>=_than c & for d be Element of L st {a,b} is_>=_than d holds c >= d proof take c = a "/\" b; a /\ b = c by A2,Th9; then c c= a & c c= b by XBOOLE_1:17; then c <= a & c <= b by Th3; hence {a,b} is_>=_than c by YELLOW_0:8; let d be Element of L; assume A3: {a,b} is_>=_than d; a in {a,b} by TARSKI:def 2; then A4: d <= a by A3,LATTICE3:def 8; b in {a,b} by TARSKI:def 2; then d <= b by A3,LATTICE3:def 8; then d c= a & d c= b by A4,Th3; then d c= a /\ b by XBOOLE_1:19; then d c= c by A2,Th9; hence c >= d by Th3; end; hence ex_inf_of {a,b},L by YELLOW_0:16; end; hence L is with_infima by YELLOW_0:21; end; theorem Th13: for X be non empty set holds {} in X implies Bottom InclPoset X = {} proof let X be non empty set; assume {} in X; then {} in the carrier of InclPoset X by Th1; then reconsider a = {} as Element of InclPoset X; A1: {} is_<=_than a by YELLOW_0:6; now let b be Element of InclPoset X; assume b in X; {} c= b by XBOOLE_1:2; hence a <= b by Th3; end; then a is_<=_than X by LATTICE3:def 8; then a is_<=_than the carrier of InclPoset X by Th1; then InclPoset X is lower-bounded by YELLOW_0:def 4; then ex_sup_of {},InclPoset X by YELLOW_0:42; then "\/"({},InclPoset X) <= a by A1,YELLOW_0:def 9; then A2: "\/"({},InclPoset X) c= a by Th3; thus Bottom InclPoset X = "\/"({},InclPoset X) by YELLOW_0:def 11 .= {} by A2,XBOOLE_1:3; end; theorem Th14: for X be non empty set holds union X in X implies Top InclPoset X = union X proof let X be non empty set; assume union X in X; then union X in the carrier of InclPoset X by Th1; then reconsider a = union X as Element of InclPoset X; "/\"({},InclPoset X) in the carrier of InclPoset X; then "/\"({},InclPoset X) in X by Th1; then A1: "/\"({},InclPoset X) c= a by ZFMISC_1:92; A2: {} is_>=_than a by YELLOW_0:6; now let b be Element of InclPoset X; assume b in X; then b c= union X by ZFMISC_1:92; hence b <= a by Th3; end; then a is_>=_than X by LATTICE3:def 9; then a is_>=_than the carrier of InclPoset X by Th1; then InclPoset X is upper-bounded by YELLOW_0:def 5; then ex_inf_of {},InclPoset X by YELLOW_0:43; then a <= "/\"({},InclPoset X) by A2,YELLOW_0:def 10; then A3: a c= "/\"({},InclPoset X) by Th3; thus Top InclPoset X = "/\"({},InclPoset X) by YELLOW_0:def 12 .= union X by A1,A3,XBOOLE_0:def 10; end; theorem for X being non empty set holds InclPoset X is upper-bounded implies union X in X proof let X be non empty set; assume InclPoset X is upper-bounded; then consider x be Element of InclPoset X such that A1: x is_>=_than the carrier of InclPoset X by YELLOW_0:def 5; x in the carrier of InclPoset X; then A2:x in X by Th1; now let y be set; assume y in union X; then consider Y be set such that A3: y in Y & Y in X by TARSKI:def 4; Y in the carrier of InclPoset X by A3,Th1; then reconsider Y as Element of InclPoset X; Y <= x by A1,LATTICE3:def 9; then Y c= x by Th3; hence y in x by A3; end; then A4: union X c= x by TARSKI:def 3; x c= union X by A2,ZFMISC_1:92; hence union X in X by A2,A4,XBOOLE_0:def 10; end; theorem for X be non empty set holds InclPoset X is lower-bounded implies meet X in X proof let X be non empty set; assume InclPoset X is lower-bounded; then consider x be Element of InclPoset X such that A1: x is_<=_than the carrier of InclPoset X by YELLOW_0:def 4; x in the carrier of InclPoset X; then A2: x in X by Th1; then A3: meet X c= x by SETFAM_1:4; now let y be set; assume A4: y in x; now let Y be set; assume Y in X; then Y in the carrier of InclPoset X by Th1; then reconsider Y' = Y as Element of InclPoset X; x <= Y' by A1,LATTICE3:def 8; then x c= Y by Th3; hence y in Y by A4; end; hence y in meet X by SETFAM_1:def 1; end; then x c= meet X by TARSKI:def 3; hence meet X in X by A2,A3,XBOOLE_0:def 10; end; Lm1: the carrier of BoolePoset X = bool X proof thus the carrier of BoolePoset X = the carrier of LattPOSet BooleLatt X by Def2 .= the carrier of RelStr (#the carrier of BooleLatt X, LattRel BooleLatt X#) by LATTICE3:def 2 .= bool X by LATTICE3:def 1; end; Lm2: for x,y be Element of BoolePoset X holds x /\ y in bool X & x \/ y in bool X proof let x,y be Element of BoolePoset X; x in the carrier of BoolePoset X & y in the carrier of BoolePoset X; then A1: x in bool X & y in bool X by Lm1; then x /\ y c= X by XBOOLE_1:108; hence x /\ y in bool X; x \/ y c= X by A1,XBOOLE_1:8; hence x \/ y in bool X; end; theorem for x,y be Element of BoolePoset X holds x "\/" y = x \/ y & x "/\" y = x /\ y proof let x,y be Element of BoolePoset X; reconsider x, y as Element of InclPoset bool X by Th4; x /\ y in bool X by Lm2; then A1: x "/\" y = x /\ y by Th9; x \/ y in bool X by Lm2; then x "\/" y = x \/ y by Th8; hence thesis by A1,Th4; end; theorem Bottom BoolePoset X = {} proof thus Bottom BoolePoset X = "\/"({},BoolePoset X) by YELLOW_0:def 11 .= "\/"({},LattPOSet BooleLatt X) by Def2 .= "\/"({},BooleLatt X) by YELLOW_0:29 .= Bottom BooleLatt X by LATTICE3:50 .= {} by LATTICE3:3; end; theorem Top BoolePoset X = X proof A1: BoolePoset X = InclPoset bool X by Th4; X in bool X by ZFMISC_1:def 1; then union bool X in bool X by ZFMISC_1:99; then Top InclPoset bool X = union bool X by Th14; hence thesis by A1,ZFMISC_1:99; end; theorem for Y being non empty Subset of BoolePoset X holds inf Y = meet Y proof set L = BoolePoset X; let Y be non empty Subset of L; A1: the carrier of L = the carrier of LattPOSet BooleLatt X by Def2 .= the carrier of RelStr(#the carrier of BooleLatt X, LattRel BooleLatt X#) by LATTICE3:def 2 .= bool X by LATTICE3:def 1; consider y being Element of Y; y c= X by A1; then meet Y c= X by SETFAM_1:8; then reconsider Me = meet Y as Element of L by A1; now let b be Element of L; assume b in Y; then Me c= b by SETFAM_1:4; hence Me <= b by Th2; end; then A2: Me is_<=_than Y by LATTICE3:def 8; now let b be Element of L; assume A3: b is_<=_than Y; now let Z be set; assume A4: Z in Y; then reconsider Z' = Z as Element of L; b <= Z' by A3,A4,LATTICE3:def 8; hence b c= Z by Th2; end; then b c= Me by SETFAM_1:6; hence Me >= b by Th2; end; hence inf Y = meet Y by A2,YELLOW_0:33; end; theorem for Y being Subset of BoolePoset X holds sup Y = union Y proof set L = BoolePoset X; let Y be Subset of L; A1: the carrier of L = the carrier of LattPOSet BooleLatt X by Def2 .= the carrier of RelStr(#the carrier of BooleLatt X, LattRel BooleLatt X#) by LATTICE3:def 2 .= bool X by LATTICE3:def 1; then union Y c= union bool X by ZFMISC_1:95; then union Y c= X by ZFMISC_1:99; then reconsider Un = union Y as Element of L by A1; now let b be Element of L; assume b in Y; then b c= Un by ZFMISC_1:92; hence b <= Un by Th2; end; then A2: Un is_>=_than Y by LATTICE3:def 9; now let b be Element of L; assume A3: b is_>=_than Y; now let Z be set; assume A4: Z in Y; then reconsider Z' = Z as Element of L; Z' <= b by A3,A4,LATTICE3:def 9; hence Z c= b by Th2; end; then Un c= b by ZFMISC_1:94; hence Un <= b by Th2; end; hence sup Y = union Y by A2,YELLOW_0:30; end; theorem for T being non empty TopSpace, X being Subset of InclPoset the topology of T holds sup X = union X proof let T be non empty TopSpace; set L = InclPoset the topology of T; reconsider t = the topology of T as non empty set; let X be Subset of L; X c= the carrier of L; then A1: X c= the topology of T by Th1; then reconsider X as Subset of bool the carrier of T by XBOOLE_1:1; reconsider X as Subset-Family of T by SETFAM_1:def 7; A2: the carrier of L = the carrier of RelStr(#t, RelIncl t#) by Def1 .= t; union X in t by A1,PRE_TOPC:def 1; then reconsider Un = union X as Element of L by A2; now let b be Element of L; assume b in X; then b c= Un by ZFMISC_1:92; hence b <= Un by Th3; end; then A3: Un is_>=_than X by LATTICE3:def 9; now let b be Element of L; assume A4: b is_>=_than X; now let Z be set; assume A5: Z in X; then reconsider Z' = Z as Element of L; Z' <= b by A4,A5,LATTICE3:def 9; hence Z c= b by Th3; end; then Un c= b by ZFMISC_1:94; hence Un <= b by Th3; end; hence thesis by A3,YELLOW_0:30; end; theorem for T be non empty TopSpace holds Bottom InclPoset the topology of T = {} proof let T be non empty TopSpace; {} in the topology of T by PRE_TOPC:5; hence thesis by Th13; end; Lm3: for T be non empty TopSpace holds InclPoset the topology of T is lower-bounded proof let T be non empty TopSpace; set L = InclPoset the topology of T; {} in the topology of T by PRE_TOPC:5; then {} in the carrier of L by Th1; then reconsider x = {} as Element of L; now take x; thus x is_<=_than the carrier of L proof let b be Element of L; assume b in the carrier of L; x c= b by XBOOLE_1:2; hence thesis by Th3; end; end; hence thesis by YELLOW_0:def 4; end; theorem for T be non empty TopSpace holds Top InclPoset the topology of T = the carrier of T proof let T be non empty TopSpace; set L = InclPoset the topology of T, C = the carrier of T; the carrier of T = "/\"({},L) proof C in the topology of T by PRE_TOPC:def 1; then C in the carrier of L by Th1; then reconsider C as Element of L; A1: C is_<=_than {} by YELLOW_0:6; for b being Element of L st b is_<=_than {} holds C >= b proof let b be Element of L; assume b is_<=_than {}; b in the carrier of L; then b in the topology of T by Th1; hence thesis by Th3; end; hence thesis by A1,YELLOW_0:31; end; hence thesis by YELLOW_0:def 12; end; Lm4: for T being non empty TopSpace holds InclPoset the topology of T is complete proof let T be non empty TopSpace; set A = the topology of T; reconsider IA = InclPoset A as lower-bounded Poset by Lm3; for X be Subset of IA holds ex_sup_of X, InclPoset A proof let X be Subset of IA; set N = union X; X c= the carrier of IA; then X c= the topology of T by Th1; then reconsider X' = X as Subset of bool the carrier of T by XBOOLE_1:1; reconsider X' as Subset-Family of T by SETFAM_1:def 7; X' c= the carrier of InclPoset A; then X' c= the topology of T by Th1; then N in the topology of T by PRE_TOPC:def 1; then N in the carrier of InclPoset A by Th1; then reconsider N as Element of InclPoset A; A1: X is_<=_than N proof let b be Element of InclPoset A; assume b in X; then b c= N by ZFMISC_1:92; hence N >= b by Th3; end; for b being Element of InclPoset A st X is_<=_than b holds N <= b proof let b be Element of InclPoset A; assume A2: X is_<=_than b; now let Z1 be set; assume A3: Z1 in X; then reconsider Z1' = Z1 as Element of InclPoset A; Z1' <= b by A2,A3,LATTICE3:def 9; hence Z1 c= b by Th3; end; then union X c= b by ZFMISC_1:94; hence thesis by Th3; end; hence thesis by A1,YELLOW_0:15; end; hence thesis by YELLOW_0:53; end; Lm5: for T being non empty TopSpace holds InclPoset the topology of T is non trivial proof let T be non empty TopSpace; set L = InclPoset the topology of T; {} in the topology of T & the carrier of T in the topology of T by PRE_TOPC:5,def 1; then {} in the carrier of L & the carrier of T in the carrier of L by Th1; then reconsider E = {}, S = the carrier of T as Element of L ; E <> S; hence thesis by REALSET1:def 20; end; definition let T be non empty TopSpace; cluster InclPoset the topology of T -> complete non trivial; coherence by Lm4,Lm5; end; theorem for T being TopSpace, F being Subset-Family of T holds F is open iff F is Subset of InclPoset the topology of T proof let T be TopSpace; let F be Subset-Family of T; hereby assume A1: F is open; F c= the topology of T proof let a be set; assume A2: a in F; then reconsider a' = a as Subset of T; a' is open by A1,A2,TOPS_2:def 1; hence thesis by PRE_TOPC:def 5; end; then F c= the carrier of InclPoset the topology of T by Th1; hence F is Subset of InclPoset the topology of T; end; assume F is Subset of InclPoset the topology of T; then F c= the carrier of InclPoset the topology of T; then A3: F c= the topology of T by Th1; let P be Subset of T; assume P in F; hence thesis by A3,PRE_TOPC:def 5; end; begin :: Products of Relational Structures reserve x,y,z for set; definition let R be Relation; attr R is RelStr-yielding means :Def3: for v being set st v in rng R holds v is RelStr; end; definition cluster RelStr-yielding -> 1-sorted-yielding Function; coherence proof let F be Function such that A1: F is RelStr-yielding; let x be set; assume x in dom F; then F.x in rng F by FUNCT_1:def 5; hence F.x is 1-sorted by A1,Def3; end; end; definition let I be set; cluster RelStr-yielding ManySortedSet of I; existence proof consider R being RelStr; take I --> R; let v be set; A1: rng(I-->R) c= {R} by FUNCOP_1:19; assume v in rng(I-->R); hence thesis by A1,TARSKI:def 1; end; end; definition let J be non empty set, A be RelStr-yielding ManySortedSet of J, j be Element of J; redefine func A.j -> RelStr; coherence proof dom A = J by PBOOLE:def 3; then A.j in rng A by FUNCT_1:def 5; hence thesis by Def3; end; end; definition let I be set; let J be RelStr-yielding ManySortedSet of I; func product J -> strict RelStr means :Def4: the carrier of it = product Carrier J & for x,y being Element of it st x in product Carrier J holds x <= y iff ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi; existence proof defpred P[set, set] means ex f,g being Function st f = $1 & g = $2 & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi; consider R being Relation of product Carrier J such that A1: for x,y being set holds [x,y] in R iff x in product Carrier J & y in product Carrier J & P[x, y] from Rel_On_Set_Ex; take RS = RelStr(#product Carrier J,R#); thus the carrier of RS = product Carrier J; let x,y be Element of RS such that A2: x in product Carrier J; hereby assume x <= y; then [x,y] in the InternalRel of RS by ORDERS_1:def 9; hence ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi by A1; end; assume ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi; then [x,y] in the InternalRel of RS by A1,A2; hence x <= y by ORDERS_1:def 9; end; uniqueness proof let S1,S2 be strict RelStr such that A3: the carrier of S1 = product Carrier J and A4: for x,y being Element of S1 st x in product Carrier J holds x <= y iff ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi and A5: the carrier of S2 = product Carrier J and A6: for x,y being Element of S2 st x in product Carrier J holds x <= y iff ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi; the InternalRel of S1 = the InternalRel of S2 proof let a,b be set; hereby assume A7: [a,b] in the InternalRel of S1; then reconsider x=a, y=b as Element of S1 by ZFMISC_1: 106; A8: a in the carrier of S1 by A7,ZFMISC_1:106; reconsider x'=x, y'=y as Element of S2 by A3,A5; x <= y by A7,ORDERS_1:def 9; then ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi by A3,A4,A8; then x' <= y' by A3,A6,A8; hence [a,b] in the InternalRel of S2 by ORDERS_1:def 9; end; assume A9: [a,b] in the InternalRel of S2; then reconsider x=a, y=b as Element of S2 by ZFMISC_1: 106; A10: a in the carrier of S2 by A9,ZFMISC_1:106; reconsider x'=x, y'=y as Element of S1 by A3,A5; x <= y by A9,ORDERS_1:def 9; then ex f,g being Function st f = x & g = y & for i be set st i in I ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi by A5,A6,A10; then x' <= y' by A4,A5,A10; hence [a,b] in the InternalRel of S1 by ORDERS_1:def 9; end; hence S1 = S2 by A3,A5; end; end; definition let X be set; let L be RelStr; cluster X --> L -> RelStr-yielding; coherence proof let v be set; A1: rng(X-->L) c= {L} by FUNCOP_1:19; assume v in rng(X-->L); hence thesis by A1,TARSKI:def 1; end; end; definition let I be set; let T be RelStr; func T|^I -> strict RelStr equals :Def5: product (I --> T); correctness; end; theorem Th26: for J be RelStr-yielding ManySortedSet of {} holds product J = RelStr (#{{}}, id {{}}#) proof let J be RelStr-yielding ManySortedSet of {}; set IT = product J; A1:the carrier of IT = product Carrier J by Def4 .= {{}} by CARD_3:19,PBOOLE:134; A2:product Carrier J = {{}} by CARD_3:19,PBOOLE:134; the InternalRel of product J = id {{}} proof let a,b be set; hereby assume [a,b] in the InternalRel of IT; then a in the carrier of IT & b in the carrier of IT by ZFMISC_1:106; then a = {} & b = {} by A1,TARSKI:def 1; then a = b & a in {{}} by TARSKI:def 1; hence [a,b] in id {{}} by RELAT_1:def 10; end; assume [a,b] in id {{}}; then A3: a in {{}} & a = b by RELAT_1:def 10; then A4: a = {} by TARSKI:def 1; reconsider x = {}, y = {} as Element of IT by A1,TARSKI:def 1; x = {} --> {{}} & y = {} --> {{}} by FUNCT_4:3; then reconsider f = x, g = y as Function; for i be set st i in {} ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi; then x <= y by A1,A2,Def4; hence thesis by A3,A4,ORDERS_1:def 9; end; hence thesis by A1; end; theorem Th27: for Y be RelStr holds Y|^{} = RelStr (#{{}}, id {{}}#) proof let Y be RelStr; Y|^{} = product ({} --> Y) by Def5; hence thesis by Th26; end; theorem Th28: for X be set, Y be RelStr holds Funcs (X, the carrier of Y) = the carrier of Y|^X proof let X be set; let Y be RelStr; set YY = the carrier of Y, f = Carrier (X --> Y); for x be set st x in X holds f.x = YY proof let x be set; assume A1: x in X; then consider R being 1-sorted such that A2: R = (X --> Y).x & f.x = the carrier of R by PRALG_1:def 13; thus thesis by A1,A2,FUNCOP_1:13; end; then A3: dom f = X & for x be set st x in X holds f.x = YY by PBOOLE:def 3; Funcs(X,YY) = product f proof thus Funcs(X,YY) c= product f proof let x be set; assume x in Funcs(X,YY); then consider g be Function such that A4: x = g & dom g = X & rng g c= YY by FUNCT_2:def 2; now let y be set; assume y in dom f; then f.y = YY & YY = YY & g.y in rng g by A3,A4,FUNCT_1:def 5; hence g.y in f.y by A4; end; hence thesis by A3,A4,CARD_3:def 5; end; let x; assume x in product f; then consider g be Function such that A5: x = g & dom g = dom f & for x st x in dom f holds g.x in f.x by CARD_3:def 5; rng g c= YY proof let y; assume y in rng g; then consider z such that A6: z in dom g & y = g.z by FUNCT_1:def 5; y in f.z & f.z = YY & YY = YY by A3,A5,A6; hence thesis; end; hence thesis by A3,A5,FUNCT_2:def 2; end; then Funcs(X,YY) = the carrier of product (X --> Y) by Def4; hence thesis by Def5; end; definition let X be set; let Y be non empty RelStr; cluster Y|^X -> non empty; coherence proof consider f be Function of X, the carrier of Y; f in Funcs (X, the carrier of Y) by FUNCT_2:11; then f in the carrier of Y|^X by Th28; hence thesis by STRUCT_0:def 1; end; end; Lm6: for X be set, Y be non empty RelStr for x be Element of Y|^X holds x in the carrier of product (X --> Y) & x is Function of X, the carrier of Y proof let X be set, Y be non empty RelStr, x be Element of Y|^X; A1: x in the carrier of Y|^X; then x in Funcs (X, the carrier of Y) by Th28; hence thesis by A1,Def5,FUNCT_2:121; end; definition let X be set; let Y be reflexive non empty RelStr; cluster Y|^X -> reflexive; coherence proof per cases; suppose X is empty; hence thesis by Th27; suppose X is non empty; then reconsider X as non empty set; for x being Element of Y|^X holds x <= x proof let x be Element of Y|^X; x in the carrier of Y|^X; then A1: x in the carrier of product (X --> Y) by Def5; reconsider x' = x as Element of product (X --> Y) by Def5; A2: x' in product Carrier (X --> Y) by A1,Def4; reconsider x1 = x as Function of X, the carrier of Y by Lm6; ex f,g being Function st f = x' & g = x' & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take x1, x1; thus x1 = x' & x1 = x'; let i be set; assume i in X; then reconsider i as Element of X; take R = (X --> Y).i; R = Y by FUNCOP_1:13; then reconsider xi = x1.i, yi = x1.i as Element of R; take xi, yi; reconsider xi1 = xi, yi1 = xi as Element of Y; xi1 <= yi1; hence thesis by FUNCOP_1:13; end; then x' <= x' by A2,Def4; then [x',x'] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [x,x] in the InternalRel of Y|^X by Def5; hence thesis by ORDERS_1:def 9; end; hence thesis by YELLOW_0:def 1; end; end; definition let Y be non empty RelStr; cluster Y|^{} -> trivial; coherence by Th27; end; definition let Y be non empty reflexive RelStr; cluster Y|^{} -> with_infima with_suprema antisymmetric; coherence; end; definition let X be set; let Y be transitive non empty RelStr; cluster Y|^X -> transitive; coherence proof set IT = Y|^X; now let x,y,z be Element of IT; A1:x in the carrier of IT & y in the carrier of IT & z in the carrier of IT; reconsider x1 = x, y1 = y, z1 = z as Element of product (X --> Y) by Def5; x1 in the carrier of product (X --> Y) & y1 in the carrier of product (X --> Y) by A1,Def5; then A2: x1 in product Carrier (X --> Y) & y1 in product Carrier (X --> Y) by Def4; assume x <= y & y <= z; then [x,y] in the InternalRel of IT & [y,z] in the InternalRel of IT by ORDERS_1:def 9; then [x1,y1] in the InternalRel of product (X --> Y) & [y1,z1] in the InternalRel of product (X --> Y) by Def5; then A3: x1 <= y1 & y1 <= z1 by ORDERS_1:def 9; then consider f,g being Function such that A4: f = x1 & g = y1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi by A2,Def4; consider f1,g1 being Function such that A5: f1 = y1 & g1 = z1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A2,A3,Def4; ex f2,g2 being Function st f2 = x1 & g2 = z1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f2.i & yi = g2.i & xi <= yi proof reconsider f2 = x, g2 = z as Function of X, the carrier of Y by Lm6; take f2, g2; thus f2 = x1 & g2 = z1; let i be set; assume A6: i in X; then reconsider X as non empty set; reconsider i as Element of X by A6; reconsider R = (X --> Y).i as RelStr; A7: R = Y by FUNCOP_1:13; then f2.i in the carrier of R & g2.i in the carrier of R by FUNCT_2:7; then reconsider xi = f2.i, yi = g2.i as Element of R; take R, xi, yi; consider R1 being RelStr, xi1,yi1 being Element of R1 such that A8: R1 = (X --> Y).i & xi1 = f.i & yi1 = g.i & xi1 <= yi1 by A4; consider R2 being RelStr, xi2,yi2 being Element of R2 such that A9: R2 = (X --> Y).i & xi2 = f1.i & yi2 = g1.i & xi2 <= yi2 by A5; thus thesis by A4,A5,A7,A8,A9,YELLOW_0:def 2; end; then x1 <= z1 by A2,Def4; then [x1, z1] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [x, z] in the InternalRel of IT by Def5; hence x <= z by ORDERS_1:def 9; end; hence thesis by YELLOW_0:def 2; end; end; definition let X be set; let Y be antisymmetric non empty RelStr; cluster Y|^X -> antisymmetric; coherence proof set IT = Y|^X; now let x,y be Element of IT; A1:x in the carrier of IT & y in the carrier of IT; reconsider x1 = x, y1 = y as Element of product (X --> Y) by Def5; x1 in the carrier of product (X --> Y) & y1 in the carrier of product (X --> Y) by A1,Def5; then A2: x1 in product Carrier (X --> Y) & y1 in product Carrier (X --> Y) by Def4; assume x <= y & y <= x; then [x,y] in the InternalRel of IT & [y,x] in the InternalRel of IT by ORDERS_1:def 9; then [x1,y1] in the InternalRel of product (X --> Y) & [y1,x1] in the InternalRel of product (X --> Y) by Def5; then A3: x1 <= y1 & y1 <= x1 by ORDERS_1:def 9; then consider f,g being Function such that A4: f = x1 & g = y1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi by A2,Def4; consider f1,g1 being Function such that A5: f1 = y1 & g1 = x1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A2,A3,Def4; reconsider x1' = x, y1' = y as Function of X, the carrier of Y by Lm6; A6: dom x1' = X & dom y1' = X by FUNCT_2:def 1; now let i be set; assume A7: i in X; then consider R1 being RelStr, xi1,yi1 being Element of R1 such that A8: R1 = (X --> Y).i & xi1 = f.i & yi1 = g.i & xi1 <= yi1 by A4; consider R2 being RelStr, xi2,yi2 being Element of R2 such that A9: R2 = (X --> Y).i & xi2 = f1.i & yi2 = g1.i & xi2 <= yi2 by A5,A7; Y = R1 & Y = R2 by A7,A8,A9,FUNCOP_1:13; hence x1'.i = y1'.i by A4,A5,A8,A9,ORDERS_1:25; end; hence x = y by A6,FUNCT_1:9; end; hence thesis by YELLOW_0:def 3; end; end; definition let X be non empty set; let Y be non empty with_infima antisymmetric RelStr; cluster Y|^X -> with_infima; coherence proof set IT = Y|^X; let x, y be Element of IT; reconsider x' = x as Function of X, the carrier of Y by Lm6; reconsider y' = y as Function of X, the carrier of Y by Lm6; defpred P[set, set] means ex xa, ya be Element of Y st xa = x'.$1 & ya = y'.$1 & $2 = xa "/\" ya; A1: for x be set st x in X ex y be set st y in the carrier of Y & P[x,y] proof let a be set; assume a in X; then x'.a in the carrier of Y & y'.a in the carrier of Y by FUNCT_2:7; then reconsider xa = x'.a, ya = y'.a as Element of Y; take y = xa "/\" ya; thus y in the carrier of Y; take xa, ya; thus thesis; end; consider f be Function of X, the carrier of Y such that A2: for a be set st a in X holds P[a,f.a] from FuncEx1(A1); f in Funcs (X, the carrier of Y) by FUNCT_2:11; then f in the carrier of IT by Th28; then reconsider z = f as Element of IT; take z; A3: z <= x proof reconsider x1 = x, z1 = z as Element of product (X --> Y) by Lm6; z1 in the carrier of IT; then z1 in the carrier of product (X --> Y) by Def5; then A4: z1 in product Carrier (X --> Y) by Def4; ex f,g being Function st f = z1 & g = x1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take f, x'; thus f = z1 & x' = x1; let i be set; assume i in X; then reconsider i as Element of X; reconsider R = (X --> Y).i as RelStr; A5: R = Y by FUNCOP_1:13; then reconsider xi = f.i, yi = x'.i as Element of R; take R, xi, yi; consider xa, ya be Element of Y such that A6: xa = x'.i & ya = y'.i & f.i = xa "/\" ya by A2; thus thesis by A5,A6,YELLOW_0:23; end; then z1 <= x1 by A4,Def4; then [z1,x1] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [z1,x1] in the InternalRel of IT by Def5; hence thesis by ORDERS_1:def 9; end; A7: z <= y proof reconsider y1 = y, z1 = z as Element of product (X --> Y) by Lm6; z1 in the carrier of IT; then z1 in the carrier of product (X --> Y) by Def5; then A8: z1 in product Carrier (X --> Y) by Def4; ex f,g being Function st f = z1 & g = y1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take f, y'; thus f = z1 & y' = y1; let i be set; assume i in X; then reconsider i as Element of X; reconsider R = (X --> Y).i as RelStr; A9: R = Y by FUNCOP_1:13; then reconsider xi = f.i, yi = y'.i as Element of R; take R, xi, yi; consider xa, ya be Element of Y such that A10: xa = x'.i & ya = y'.i & f.i = xa "/\" ya by A2; thus thesis by A9,A10,YELLOW_0:23; end; then z1 <= y1 by A8,Def4; then [z1,y1] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [z1,y1] in the InternalRel of IT by Def5; hence thesis by ORDERS_1:def 9; end; for z' being Element of IT st z' <= x & z' <= y holds z' <= z proof let z' be Element of IT; assume A11: z' <= x & z' <= y; z' <= z proof reconsider z2 = z', z3 = z, z4 = y, z5 = x as Element of the carrier of product (X --> Y) by Lm6; reconsider J = z2, K = z3 as Function of X, the carrier of Y by Lm6; z' in the carrier of product (X --> Y) by Lm6; then A12: z2 in product Carrier (X --> Y) by Def4; [z',x] in the InternalRel of IT by A11,ORDERS_1:def 9; then A13: [z2,z5] in the InternalRel of product (X --> Y) by Def5; [z',y] in the InternalRel of IT by A11,ORDERS_1:def 9; then [z2,z4] in the InternalRel of product (X --> Y) by Def5; then A14: z2 <= z5 & z2 <= z4 by A13,ORDERS_1:def 9; then consider f1,g1 being Function such that A15: f1 = z2 & g1 = z5 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A12,Def4; consider f2,g2 being Function such that A16: f2 = z2 & g2 = z4 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f2.i & yi = g2.i & xi <= yi by A12,A14,Def4; ex f,g being Function st f = z2 & g = z3 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take J, K; thus J = z2 & K = z3; let i be set; assume i in X; then reconsider i as Element of X; reconsider R = (X --> Y).i as RelStr; A17: R = Y by FUNCOP_1:13; then reconsider xi = J.i, yi = K.i as Element of R; take R, xi, yi; consider xa, ya be Element of Y such that A18: xa = x'.i & ya = y'.i & f.i = xa "/\" ya by A2; consider R1 being RelStr, xi1,yi1 being Element of R1 such that A19: R1 = (X --> Y).i & xi1 = f1.i & yi1 = g1.i & xi1 <= yi1 by A15; consider R2 being RelStr, xi2,yi2 being Element of R2 such that A20: R2 = (X --> Y).i & xi2 = f2.i & yi2 = g2.i & xi2 <= yi2 by A16; thus thesis by A15,A16,A17,A18,A19,A20,YELLOW_0:23; end; then z2 <= z3 by A12,Def4; then [z2,z3] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [z2,z3] in the InternalRel of IT by Def5; hence thesis by ORDERS_1:def 9; end; hence thesis; end; hence thesis by A3,A7; end; end; definition let X be non empty set; let Y be non empty with_suprema antisymmetric RelStr; cluster Y|^X -> with_suprema; coherence proof set IT = Y|^X; let x, y be Element of IT; reconsider x' = x as Function of X, the carrier of Y by Lm6; reconsider y' = y as Function of X, the carrier of Y by Lm6; defpred P[set, set] means ex xa, ya be Element of Y st xa = x'.$1 & ya = y'.$1 & $2 = xa "\/" ya; A1: for x be set st x in X ex y be set st y in the carrier of Y & P[x,y] proof let a be set; assume a in X; then x'.a in the carrier of Y & y'.a in the carrier of Y by FUNCT_2:7; then reconsider xa = x'.a, ya = y'.a as Element of Y; take y = xa "\/" ya; thus y in the carrier of Y; take xa, ya; thus thesis; end; consider f be Function of X, the carrier of Y such that A2: for a be set st a in X holds P[a,f.a] from FuncEx1(A1); f in Funcs (X, the carrier of Y) by FUNCT_2:11; then f in the carrier of IT by Th28; then reconsider z = f as Element of IT; take z; A3: x <= z proof reconsider x1 = x, z1 = z as Element of product (X --> Y) by Lm6; x1 in the carrier of product (X --> Y) by Lm6; then A4: x1 in product Carrier (X --> Y) by Def4; ex f,g being Function st f = x1 & g = z1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take x',f; thus x' = x1 & f = z1; let i be set; assume i in X; then reconsider i as Element of X; reconsider R = (X --> Y).i as RelStr; A5: R = Y by FUNCOP_1:13; then reconsider yi = f.i, xi = x'.i as Element of R; take R, xi, yi; consider xa, ya be Element of Y such that A6: xa = x'.i & ya = y'.i & f.i = xa "\/" ya by A2; thus thesis by A5,A6,YELLOW_0:22; end; then x1 <= z1 by A4,Def4; then [x1,z1] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [x1,z1] in the InternalRel of IT by Def5; hence thesis by ORDERS_1:def 9; end; A7: y <= z proof reconsider y1 = y, z1 = z as Element of product (X --> Y) by Lm6; y1 in the carrier of product (X --> Y) by Lm6; then A8: y1 in product Carrier (X --> Y) by Def4; ex f,g being Function st f = y1 & g = z1 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take y', f; thus y' = y1 & f = z1; let i be set; assume i in X; then reconsider i as Element of X; reconsider R = (X --> Y).i as RelStr; A9: R = Y by FUNCOP_1:13; then reconsider yi = f.i, xi = y'.i as Element of R; take R, xi, yi; consider xa, ya be Element of Y such that A10: xa = x'.i & ya = y'.i & f.i = xa "\/" ya by A2; thus thesis by A9,A10,YELLOW_0:22; end; then y1 <= z1 by A8,Def4; then [y1,z1] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [y1,z1] in the InternalRel of IT by Def5; hence thesis by ORDERS_1:def 9; end; for z' being Element of IT st z' >= x & z' >= y holds z' >= z proof let z' be Element of IT; assume A11: z' >= x & z' >= y; z' >= z proof reconsider z2 = z', z3 = z, z4 = y, z5 = x as Element of the carrier of product (X --> Y) by Lm6; reconsider K = z3, J = z2 as Function of X, the carrier of Y by Lm6; z5 in the carrier of product (X --> Y) & z3 in the carrier of product (X --> Y) & z4 in the carrier of product (X --> Y) by Lm6; then A12: z5 in product Carrier (X --> Y) & z3 in product Carrier (X --> Y) & z4 in product Carrier (X --> Y) by Def4; [x, z'] in the InternalRel of IT by A11,ORDERS_1:def 9; then A13: [z5,z2] in the InternalRel of product (X --> Y) by Def5; [y, z'] in the InternalRel of IT by A11,ORDERS_1:def 9; then [z4,z2] in the InternalRel of product (X --> Y) by Def5; then A14: z5 <= z2 & z4 <= z2 by A13,ORDERS_1:def 9; then consider f1,g1 being Function such that A15: f1 = z5 & g1 = z2 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A12,Def4; consider f2,g2 being Function such that A16: f2 = z4 & g2 = z2 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f2.i & yi = g2.i & xi <= yi by A12,A14,Def4; ex f,g being Function st f = z3 & g = z2 & for i be set st i in X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi proof take K, J; thus K = z3 & J = z2; let i be set; assume i in X; then reconsider i as Element of X; reconsider R = (X --> Y).i as RelStr; A17: R = Y by FUNCOP_1:13; then reconsider yi = J.i, xi = K.i as Element of R; take R, xi, yi; consider xa, ya be Element of Y such that A18: xa = x'.i & ya = y'.i & f.i = xa "\/" ya by A2; consider R1 being RelStr, xi1,yi1 being Element of R1 such that A19: R1 = (X --> Y).i & xi1 = f1.i & yi1 = g1.i & xi1 <= yi1 by A15; consider R2 being RelStr, xi2,yi2 being Element of R2 such that A20: R2 = (X --> Y).i & xi2 = f2.i & yi2 = g2.i & xi2 <= yi2 by A16; thus thesis by A15,A16,A17,A18,A19,A20,YELLOW_0:22; end; then z3 <= z2 by A12,Def4; then [z3,z2] in the InternalRel of product (X --> Y) by ORDERS_1:def 9; then [z3,z2] in the InternalRel of IT by Def5; hence thesis by ORDERS_1:def 9; end; hence thesis; end; hence thesis by A3,A7; end; end; definition let S,T be RelStr; func MonMaps (S,T) -> strict full SubRelStr of T|^the carrier of S means for f being map of S,T holds f in the carrier of it iff f in Funcs (the carrier of S, the carrier of T) & f is monotone; existence proof set X = MonFuncs (S,T); X c= Funcs (the carrier of S, the carrier of T) by ORDERS_3:11; then reconsider X as Subset of T|^the carrier of S by Th28; take SX = subrelstr X; let f be map of S,T; hereby assume f in the carrier of SX; then f in X by YELLOW_0:def 15; then consider f' be map of S, T such that A1: f' = f & f' in Funcs (the carrier of S, the carrier of T) & f' is monotone by ORDERS_3:def 6; thus f in Funcs (the carrier of S, the carrier of T) & f is monotone by A1; end; assume f in Funcs (the carrier of S, the carrier of T) & f is monotone; then f in X by ORDERS_3:def 6; hence f in the carrier of SX by YELLOW_0:def 15; end; uniqueness proof let A1, A2 be strict full SubRelStr of T|^the carrier of S; assume that A2: for f being map of S,T holds f in the carrier of A1 iff f in Funcs (the carrier of S, the carrier of T) & f is monotone and A3: for f being map of S,T holds f in the carrier of A2 iff f in Funcs (the carrier of S, the carrier of T) & f is monotone; the carrier of A1 c= the carrier of T|^the carrier of S by YELLOW_0:def 13; then A4:the carrier of A1 c= Funcs (the carrier of S, the carrier of T) by Th28 ; the carrier of A2 c= the carrier of T|^the carrier of S by YELLOW_0:def 13; then A5:the carrier of A2 c= Funcs (the carrier of S, the carrier of T) by Th28; set X = the carrier of S, Y = the carrier of T; the carrier of A1 = the carrier of A2 proof thus the carrier of A1 c= the carrier of A2 proof let a be set; assume A6: a in the carrier of A1; then a is Function of X, Y by A4,FUNCT_2:121; then reconsider f = a as map of S, T; f is monotone by A2,A6; hence a in the carrier of A2 by A3,A4,A6; end; thus the carrier of A2 c= the carrier of A1 proof let a be set; assume A7: a in the carrier of A2; then a is Function of X, Y by A5,FUNCT_2:121; then reconsider f = a as map of S, T; f is monotone by A3,A7; hence a in the carrier of A1 by A2,A5,A7; end; end; hence thesis by YELLOW_0:58; end; end;

Back to top