:: WAYBEL_5 semantic presentation begin Lm1: for L being continuous Semilattice for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) proof let L be continuous Semilattice; ::_thesis: for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) let x be Element of L; ::_thesis: ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) thus waybelow x is Ideal of L ; ::_thesis: ( x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) thus x <= sup (waybelow x) by WAYBEL_3:def_5; ::_thesis: for I being Ideal of L st x <= sup I holds waybelow x c= I thus for I being Ideal of L st x <= sup I holds waybelow x c= I ::_thesis: verum proof let I be Ideal of L; ::_thesis: ( x <= sup I implies waybelow x c= I ) assume A1: x <= sup I ; ::_thesis: waybelow x c= I waybelow x c= I proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in waybelow x or y in I ) assume y in waybelow x ; ::_thesis: y in I then y in { y9 where y9 is Element of L : y9 << x } by WAYBEL_3:def_3; then ex y9 being Element of L st ( y = y9 & y9 << x ) ; hence y in I by A1, WAYBEL_3:20; ::_thesis: verum end; hence waybelow x c= I ; ::_thesis: verum end; end; Lm2: for L being up-complete Semilattice st ( for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) ) holds L is continuous proof let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) ) implies L is continuous ) assume A1: for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) ; ::_thesis: L is continuous now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x) let x be Element of L; ::_thesis: x = sup (waybelow x) A2: x <= sup (waybelow x) by A1; ( not waybelow x is empty & waybelow x is directed ) by A1; then A3: ex_sup_of waybelow x,L by WAYBEL_0:75; waybelow x is_<=_than x by WAYBEL_3:9; then sup (waybelow x) <= x by A3, YELLOW_0:def_9; hence x = sup (waybelow x) by A2, YELLOW_0:def_3; ::_thesis: verum end; then A4: L is satisfying_axiom_of_approximation by WAYBEL_3:def_5; for x being Element of L holds ( not waybelow x is empty & waybelow x is directed ) by A1; hence L is continuous by A4, WAYBEL_3:def_6; ::_thesis: verum end; theorem :: WAYBEL_5:1 for L being up-complete Semilattice holds ( L is continuous iff for x being Element of L holds ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) ) by Lm1, Lm2; Lm3: for L being up-complete Semilattice st L is continuous holds for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) proof let L be up-complete Semilattice; ::_thesis: ( L is continuous implies for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ) assume A1: L is continuous ; ::_thesis: for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) let x be Element of L; ::_thesis: ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) reconsider I = waybelow x as Ideal of L by A1; take I ; ::_thesis: ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) thus ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) by A1, Lm1; ::_thesis: verum end; Lm4: for L being up-complete Semilattice st ( for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ) holds L is continuous proof let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ) implies L is continuous ) assume A1: for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ; ::_thesis: L is continuous now__::_thesis:_for_x_being_Element_of_L_holds_ (_waybelow_x_is_Ideal_of_L_&_x_<=_sup_(waybelow_x)_&_(_for_I_being_Ideal_of_L_st_x_<=_sup_I_holds_ waybelow_x_c=_I_)_) let x be Element of L; ::_thesis: ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) consider I being Ideal of L such that A2: x <= sup I and A3: for J being Ideal of L st x <= sup J holds I c= J by A1; now__::_thesis:_for_y_being_set_st_y_in_I_holds_ y_in_waybelow_x let y be set ; ::_thesis: ( y in I implies y in waybelow x ) assume A4: y in I ; ::_thesis: y in waybelow x then reconsider y9 = y as Element of L ; for J being Ideal of L st x <= sup J holds y in J proof let J be Ideal of L; ::_thesis: ( x <= sup J implies y in J ) assume x <= sup J ; ::_thesis: y in J then I c= J by A3; hence y in J by A4; ::_thesis: verum end; then y9 << x by WAYBEL_3:21; hence y in waybelow x by WAYBEL_3:7; ::_thesis: verum end; then A5: I c= waybelow x by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_waybelow_x_holds_ y_in_I let y be set ; ::_thesis: ( y in waybelow x implies y in I ) assume A6: y in waybelow x ; ::_thesis: y in I then reconsider y9 = y as Element of L ; y9 << x by A6, WAYBEL_3:7; hence y in I by A2, WAYBEL_3:20; ::_thesis: verum end; then waybelow x c= I by TARSKI:def_3; then waybelow x = I by A5, XBOOLE_0:def_10; hence ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds waybelow x c= I ) ) by A2, A3; ::_thesis: verum end; hence L is continuous by Lm2; ::_thesis: verum end; theorem :: WAYBEL_5:2 for L being up-complete Semilattice holds ( L is continuous iff for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) ) by Lm3, Lm4; theorem :: WAYBEL_5:3 for L being lower-bounded continuous sup-Semilattice holds SupMap L is upper_adjoint proof let L be lower-bounded continuous sup-Semilattice; ::_thesis: SupMap L is upper_adjoint set P = InclPoset (Ids L); set r = SupMap L; deffunc H1( Element of L) -> Element of the carrier of (InclPoset (Ids L)) = inf ((SupMap L) " (uparrow {\$1})); ex d being Function of L,(InclPoset (Ids L)) st for t being Element of L holds d . t = H1(t) from FUNCT_2:sch_4(); then consider d being Function of L,(InclPoset (Ids L)) such that A1: for t being Element of L holds d . t = inf ((SupMap L) " (uparrow {t})) ; for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t) proof let t be Element of L; ::_thesis: d . t is_minimum_of (SupMap L) " (uparrow t) set I = inf ((SupMap L) " (uparrow t)); reconsider I9 = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:41; A2: d . t = inf ((SupMap L) " (uparrow {t})) by A1 .= inf ((SupMap L) " (uparrow t)) by WAYBEL_0:def_18 ; inf ((SupMap L) " (uparrow t)) in the carrier of (InclPoset (Ids L)) ; then inf ((SupMap L) " (uparrow t)) in Ids L by YELLOW_1:1; then A3: inf ((SupMap L) " (uparrow t)) in dom (SupMap L) by YELLOW_2:49; consider J being Ideal of L such that A4: t <= sup J and A5: for K being Ideal of L st t <= sup K holds J c= K by Lm3; reconsider J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41; A6: for K being Element of (InclPoset (Ids L)) st (SupMap L) " (uparrow t) is_>=_than K holds K <= J9 proof J9 in the carrier of (InclPoset (Ids L)) ; then J9 in Ids L by YELLOW_1:1; then A7: J in dom (SupMap L) by YELLOW_2:49; let K be Element of (InclPoset (Ids L)); ::_thesis: ( (SupMap L) " (uparrow t) is_>=_than K implies K <= J9 ) assume A8: (SupMap L) " (uparrow t) is_>=_than K ; ::_thesis: K <= J9 t <= (SupMap L) . J9 by A4, YELLOW_2:def_3; then (SupMap L) . J in uparrow t by WAYBEL_0:18; then J in (SupMap L) " (uparrow t) by A7, FUNCT_1:def_7; hence K <= J9 by A8, LATTICE3:def_8; ::_thesis: verum end; (SupMap L) " (uparrow t) is_>=_than J9 proof let K be Element of (InclPoset (Ids L)); :: according to LATTICE3:def_8 ::_thesis: ( not K in (SupMap L) " (uparrow t) or J9 <= K ) reconsider K9 = K as Ideal of L by YELLOW_2:41; assume K in (SupMap L) " (uparrow t) ; ::_thesis: J9 <= K then (SupMap L) . K in uparrow t by FUNCT_1:def_7; then t <= (SupMap L) . K by WAYBEL_0:18; then t <= sup K9 by YELLOW_2:def_3; then J9 c= K9 by A5; hence J9 <= K by YELLOW_1:3; ::_thesis: verum end; then t <= sup I9 by A4, A6, YELLOW_0:31; then t <= (SupMap L) . (inf ((SupMap L) " (uparrow t))) by YELLOW_2:def_3; then (SupMap L) . (inf ((SupMap L) " (uparrow t))) in uparrow t by WAYBEL_0:18; then ( ex_inf_of (SupMap L) " (uparrow t), InclPoset (Ids L) & inf ((SupMap L) " (uparrow t)) in (SupMap L) " (uparrow t) ) by A3, FUNCT_1:def_7, YELLOW_0:17; hence d . t is_minimum_of (SupMap L) " (uparrow t) by A2, WAYBEL_1:def_6; ::_thesis: verum end; then [(SupMap L),d] is Galois by WAYBEL_1:10; hence SupMap L is upper_adjoint by WAYBEL_1:def_11; ::_thesis: verum end; theorem :: WAYBEL_5:4 for L being lower-bounded up-complete LATTICE st SupMap L is upper_adjoint holds L is continuous proof let L be lower-bounded up-complete LATTICE; ::_thesis: ( SupMap L is upper_adjoint implies L is continuous ) set P = InclPoset (Ids L); assume A1: SupMap L is upper_adjoint ; ::_thesis: L is continuous for x being Element of L ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) proof set r = SupMap L; let x be Element of L; ::_thesis: ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) set I9 = inf ((SupMap L) " (uparrow x)); reconsider I = inf ((SupMap L) " (uparrow x)) as Ideal of L by YELLOW_2:41; A2: for J being Ideal of L st x <= sup J holds I c= J proof let J be Ideal of L; ::_thesis: ( x <= sup J implies I c= J ) reconsider J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41; assume x <= sup J ; ::_thesis: I c= J then x <= (SupMap L) . J9 by YELLOW_2:def_3; then ( J in dom (SupMap L) & (SupMap L) . J9 in uparrow x ) by WAYBEL_0:18, YELLOW_2:50; then J9 in (SupMap L) " (uparrow x) by FUNCT_1:def_7; then inf ((SupMap L) " (uparrow x)) <= J9 by YELLOW_2:22; hence I c= J by YELLOW_1:3; ::_thesis: verum end; consider d being Function of L,(InclPoset (Ids L)) such that A3: [(SupMap L),d] is Galois by A1, WAYBEL_1:def_11; d . x is_minimum_of (SupMap L) " (uparrow x) by A3, WAYBEL_1:10; then I in (SupMap L) " (uparrow x) by WAYBEL_1:def_6; then (SupMap L) . I in uparrow x by FUNCT_1:def_7; then x <= (SupMap L) . (inf ((SupMap L) " (uparrow x))) by WAYBEL_0:18; then x <= sup I by YELLOW_2:def_3; hence ex I being Ideal of L st ( x <= sup I & ( for J being Ideal of L st x <= sup J holds I c= J ) ) by A2; ::_thesis: verum end; hence L is continuous by Lm4; ::_thesis: verum end; theorem :: WAYBEL_5:5 for L being complete Semilattice st SupMap L is infs-preserving & SupMap L is sups-preserving holds SupMap L is upper_adjoint proof let L be complete Semilattice; ::_thesis: ( SupMap L is infs-preserving & SupMap L is sups-preserving implies SupMap L is upper_adjoint ) set r = SupMap L; assume ( SupMap L is infs-preserving & SupMap L is sups-preserving ) ; ::_thesis: SupMap L is upper_adjoint then ex d being Function of L,(InclPoset (Ids L)) st ( [(SupMap L),d] is Galois & ( for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t) ) ) by WAYBEL_1:14; hence SupMap L is upper_adjoint by WAYBEL_1:def_11; ::_thesis: verum end; definition let J, D be set ; let K be ManySortedSet of J; mode DoubleIndexedSet of K,D is ManySortedFunction of K,J --> D; end; definition let J be set ; let K be ManySortedSet of J; let S be 1-sorted ; mode DoubleIndexedSet of K,S is DoubleIndexedSet of K, the carrier of S; end; theorem Th6: :: WAYBEL_5:6 for J, D being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for j being set st j in J holds F . j is Function of (K . j),D proof let J, D be set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for j being set st j in J holds F . j is Function of (K . j),D let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,D for j being set st j in J holds F . j is Function of (K . j),D let F be DoubleIndexedSet of K,D; ::_thesis: for j being set st j in J holds F . j is Function of (K . j),D let j be set ; ::_thesis: ( j in J implies F . j is Function of (K . j),D ) assume A1: j in J ; ::_thesis: F . j is Function of (K . j),D then (J --> D) . j = D by FUNCOP_1:7; hence F . j is Function of (K . j),D by A1, PBOOLE:def_15; ::_thesis: verum end; definition let J, D be non empty set ; let K be ManySortedSet of J; let F be DoubleIndexedSet of K,D; let j be Element of J; :: original: . redefine funcF . j -> Function of (K . j),D; coherence F . j is Function of (K . j),D by Th6; end; registration let J, D be non empty set ; let K be V9() ManySortedSet of J; let F be DoubleIndexedSet of K,D; let j be Element of J; cluster proj2 (F . j) -> non empty ; correctness coherence not rng (F . j) is empty ; ; end; registration let J be set ; let D be non empty set ; let K be V9() ManySortedSet of J; cluster -> V9() for ManySortedFunction of K,J --> D; correctness coherence for b1 being DoubleIndexedSet of K,D holds b1 is V9(); proof let F be DoubleIndexedSet of K,D; ::_thesis: F is V9() for j being set st j in dom F holds not F . j is empty proof let j be set ; ::_thesis: ( j in dom F implies not F . j is empty ) set k = the Element of K . j; assume j in dom F ; ::_thesis: not F . j is empty then A1: j in J ; then F . j is Function of (K . j),D by Th6; then dom (F . j) = K . j by FUNCT_2:def_1; then [ the Element of K . j,((F . j) . the Element of K . j)] in F . j by A1, FUNCT_1:def_2; hence not F . j is empty ; ::_thesis: verum end; hence F is V9() by FUNCT_1:def_9; ::_thesis: verum end; end; theorem :: WAYBEL_5:7 for F being Function-yielding Function for f being set st f in dom (Frege F) holds f is Function ; theorem Th8: :: WAYBEL_5:8 for F being Function-yielding Function for f being Function st f in dom (Frege F) holds ( dom f = dom F & dom F = dom ((Frege F) . f) ) proof let F be Function-yielding Function; ::_thesis: for f being Function st f in dom (Frege F) holds ( dom f = dom F & dom F = dom ((Frege F) . f) ) let f be Function; ::_thesis: ( f in dom (Frege F) implies ( dom f = dom F & dom F = dom ((Frege F) . f) ) ) assume f in dom (Frege F) ; ::_thesis: ( dom f = dom F & dom F = dom ((Frege F) . f) ) then A1: f in product (doms F) ; then ex g being Function st ( g = f & dom g = dom (doms F) & ( for x being set st x in dom (doms F) holds g . x in (doms F) . x ) ) by CARD_3:def_5; hence dom f = dom F by FUNCT_6:59; ::_thesis: dom F = dom ((Frege F) . f) thus dom ((Frege F) . f) = dom (F .. f) by A1, PRALG_2:def_2 .= dom F by PRALG_1:def_17 ; ::_thesis: verum end; theorem Th9: :: WAYBEL_5:9 for F being Function-yielding Function for f being Function st f in dom (Frege F) holds for i being set st i in dom F holds ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) proof let F be Function-yielding Function; ::_thesis: for f being Function st f in dom (Frege F) holds for i being set st i in dom F holds ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) let f be Function; ::_thesis: ( f in dom (Frege F) implies for i being set st i in dom F holds ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) ) assume A1: f in dom (Frege F) ; ::_thesis: for i being set st i in dom F holds ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) A2: f in product (doms F) by A1; set G = (Frege F) . f; let i be set ; ::_thesis: ( i in dom F implies ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) ) assume A3: i in dom F ; ::_thesis: ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) i in dom (doms F) by A3, FUNCT_6:59; then f . i in (doms F) . i by A2, CARD_3:9; hence f . i in dom (F . i) by A3, FUNCT_6:22; ::_thesis: ( ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) (Frege F) . f = F .. f by A2, PRALG_2:def_2; hence A4: ((Frege F) . f) . i = (F . i) . (f . i) by A3, PRALG_1:def_17; ::_thesis: (F . i) . (f . i) in rng ((Frege F) . f) dom ((Frege F) . f) = dom F by A1, Th8; hence (F . i) . (f . i) in rng ((Frege F) . f) by A3, A4, FUNCT_1:def_3; ::_thesis: verum end; theorem Th10: :: WAYBEL_5:10 for J, D being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds (Frege F) . f is Function of J,D proof let J, D be set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds (Frege F) . f is Function of J,D let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds (Frege F) . f is Function of J,D let F be DoubleIndexedSet of K,D; ::_thesis: for f being Function st f in dom (Frege F) holds (Frege F) . f is Function of J,D let f be Function; ::_thesis: ( f in dom (Frege F) implies (Frege F) . f is Function of J,D ) assume A1: f in dom (Frege F) ; ::_thesis: (Frege F) . f is Function of J,D set G = (Frege F) . f; A2: dom ((Frege F) . f) = dom F by A1, Th8; A3: dom F = J by PARTFUN1:def_2; rng ((Frege F) . f) c= D proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((Frege F) . f) or y in D ) assume y in rng ((Frege F) . f) ; ::_thesis: y in D then consider x being set such that A4: x in dom ((Frege F) . f) and A5: y = ((Frege F) . f) . x by FUNCT_1:def_3; F . x is Function of (K . x),D by A2, A4, Th6; then A6: rng (F . x) c= D by RELAT_1:def_19; ( ((Frege F) . f) . x = (F . x) . (f . x) & f . x in dom (F . x) ) by A1, A2, A4, Th9; then y in rng (F . x) by A5, FUNCT_1:def_3; hence y in D by A6; ::_thesis: verum end; hence (Frege F) . f is Function of J,D by A3, A2, FUNCT_2:2; ::_thesis: verum end; Lm5: for J, D being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) proof let J, D be set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) let F be DoubleIndexedSet of K,D; ::_thesis: for f being Function st f in dom (Frege F) holds for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) let f be Function; ::_thesis: ( f in dom (Frege F) implies for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) ) assume A1: f in dom (Frege F) ; ::_thesis: for j being set st j in J holds ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) let j be set ; ::_thesis: ( j in J implies ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) ) assume j in J ; ::_thesis: ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) then A2: j in dom F by PARTFUN1:def_2; hence ((Frege F) . f) . j = (F . j) . (f . j) by A1, Th9; ::_thesis: (F . j) . (f . j) in rng ((Frege F) . f) thus (F . j) . (f . j) in rng ((Frege F) . f) by A1, A2, Th9; ::_thesis: verum end; Lm6: for J being set for K being ManySortedSet of J for D being non empty set for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds f . j in K . j proof let J be set ; ::_thesis: for K being ManySortedSet of J for D being non empty set for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds f . j in K . j let K be ManySortedSet of J; ::_thesis: for D being non empty set for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds f . j in K . j let D be non empty set ; ::_thesis: for F being DoubleIndexedSet of K,D for f being Function st f in dom (Frege F) holds for j being set st j in J holds f . j in K . j let F be DoubleIndexedSet of K,D; ::_thesis: for f being Function st f in dom (Frege F) holds for j being set st j in J holds f . j in K . j let f be Function; ::_thesis: ( f in dom (Frege F) implies for j being set st j in J holds f . j in K . j ) assume A1: f in dom (Frege F) ; ::_thesis: for j being set st j in J holds f . j in K . j let j be set ; ::_thesis: ( j in J implies f . j in K . j ) assume A2: j in J ; ::_thesis: f . j in K . j A3: F . j is Function of (K . j),D by A2, Th6; dom F = J by PARTFUN1:def_2; then f . j in dom (F . j) by A1, A2, Th9; hence f . j in K . j by A3, FUNCT_2:def_1; ::_thesis: verum end; registration let f be non-empty Function; cluster doms f -> non-empty ; correctness coherence doms f is non-empty ; proof for j being set st j in dom (doms f) holds not (doms f) . j is empty proof let j be set ; ::_thesis: ( j in dom (doms f) implies not (doms f) . j is empty ) assume that A1: j in dom (doms f) and A2: (doms f) . j is empty ; ::_thesis: contradiction A3: j in f " (SubFuncs (rng f)) by A1, FUNCT_6:def_2; then reconsider fj = f . j as Function by FUNCT_6:19; A4: j in dom f by A3, FUNCT_6:19; then {} = dom fj by A2, FUNCT_6:22; then f . j = {} ; hence contradiction by A4, FUNCT_1:def_9; ::_thesis: verum end; hence doms f is non-empty by FUNCT_1:def_9; ::_thesis: verum end; end; definition let J, D be set ; let K be ManySortedSet of J; let F be DoubleIndexedSet of K,D; :: original: Frege redefine func Frege F -> DoubleIndexedSet of (product (doms F)) --> J,D; coherence Frege F is DoubleIndexedSet of (product (doms F)) --> J,D proof set G = Frege F; set PD = product (doms F); set A = (product (doms F)) --> J; set B = (product (doms F)) --> D; for i being set st i in product (doms F) holds (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) proof let i be set ; ::_thesis: ( i in product (doms F) implies (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) ) assume A1: i in product (doms F) ; ::_thesis: (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) then reconsider f = i as Function ; A2: ((product (doms F)) --> D) . i = D by A1, FUNCOP_1:7; ( i in dom (Frege F) & ((product (doms F)) --> J) . i = J ) by A1, FUNCOP_1:7, PARTFUN1:def_2; then (Frege F) . f is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) by A2, Th10; hence (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) ; ::_thesis: verum end; hence Frege F is DoubleIndexedSet of (product (doms F)) --> J,D by PBOOLE:def_15; ::_thesis: verum end; end; definition let J, D be non empty set ; let K be V9() ManySortedSet of J; let F be DoubleIndexedSet of K,D; let G be DoubleIndexedSet of (product (doms F)) --> J,D; let f be Element of product (doms F); :: original: . redefine funcG . f -> Function of J,D; coherence G . f is Function of J,D proof ((product (doms F)) --> J) . f = J by FUNCOP_1:7; hence G . f is Function of J,D ; ::_thesis: verum end; end; definition let L be non empty RelStr ; let F be Function-yielding Function; func \// (F,L) -> Function of (dom F), the carrier of L means :Def1: :: WAYBEL_5:def 1 for x being set st x in dom F holds it . x = \\/ ((F . x),L); existence ex b1 being Function of (dom F), the carrier of L st for x being set st x in dom F holds b1 . x = \\/ ((F . x),L) proof deffunc H1( set ) -> Element of the carrier of L = \\/ ((F . \$1),L); ex f being Function st ( dom f = dom F & ( for x being set st x in dom F holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); then consider f being Function such that A1: dom f = dom F and A2: for x being set st x in dom F holds f . x = \\/ ((F . x),L) ; rng f c= the carrier of L proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of L ) assume y in rng f ; ::_thesis: y in the carrier of L then consider x being set such that A3: ( x in dom f & y = f . x ) by FUNCT_1:def_3; y = \\/ ((F . x),L) by A1, A2, A3; hence y in the carrier of L ; ::_thesis: verum end; then reconsider f = f as Function of (dom F), the carrier of L by A1, FUNCT_2:2; take f ; ::_thesis: for x being set st x in dom F holds f . x = \\/ ((F . x),L) thus for x being set st x in dom F holds f . x = \\/ ((F . x),L) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds b1 . x = \\/ ((F . x),L) ) & ( for x being set st x in dom F holds b2 . x = \\/ ((F . x),L) ) holds b1 = b2 proof let f, g be Function of (dom F), the carrier of L; ::_thesis: ( ( for x being set st x in dom F holds f . x = \\/ ((F . x),L) ) & ( for x being set st x in dom F holds g . x = \\/ ((F . x),L) ) implies f = g ) assume that A4: for x being set st x in dom F holds f . x = \\/ ((F . x),L) and A5: for x being set st x in dom F holds g . x = \\/ ((F . x),L) ; ::_thesis: f = g A6: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom F implies f . x = g . x ) assume A7: x in dom F ; ::_thesis: f . x = g . x hence f . x = \\/ ((F . x),L) by A4 .= g . x by A5, A7 ; ::_thesis: verum end; ( dom f = dom F & dom g = dom F ) by FUNCT_2:def_1; hence f = g by A6, FUNCT_1:2; ::_thesis: verum end; func /\\ (F,L) -> Function of (dom F), the carrier of L means :Def2: :: WAYBEL_5:def 2 for x being set st x in dom F holds it . x = //\ ((F . x),L); existence ex b1 being Function of (dom F), the carrier of L st for x being set st x in dom F holds b1 . x = //\ ((F . x),L) proof deffunc H1( set ) -> Element of the carrier of L = //\ ((F . \$1),L); ex f being Function st ( dom f = dom F & ( for x being set st x in dom F holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); then consider f being Function such that A8: dom f = dom F and A9: for x being set st x in dom F holds f . x = //\ ((F . x),L) ; rng f c= the carrier of L proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of L ) assume y in rng f ; ::_thesis: y in the carrier of L then consider x being set such that A10: ( x in dom f & y = f . x ) by FUNCT_1:def_3; y = //\ ((F . x),L) by A8, A9, A10; hence y in the carrier of L ; ::_thesis: verum end; then reconsider f = f as Function of (dom F), the carrier of L by A8, FUNCT_2:2; take f ; ::_thesis: for x being set st x in dom F holds f . x = //\ ((F . x),L) thus for x being set st x in dom F holds f . x = //\ ((F . x),L) by A9; ::_thesis: verum end; uniqueness for b1, b2 being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds b1 . x = //\ ((F . x),L) ) & ( for x being set st x in dom F holds b2 . x = //\ ((F . x),L) ) holds b1 = b2 proof let f, g be Function of (dom F), the carrier of L; ::_thesis: ( ( for x being set st x in dom F holds f . x = //\ ((F . x),L) ) & ( for x being set st x in dom F holds g . x = //\ ((F . x),L) ) implies f = g ) assume that A11: for x being set st x in dom F holds f . x = //\ ((F . x),L) and A12: for x being set st x in dom F holds g . x = //\ ((F . x),L) ; ::_thesis: f = g A13: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom F implies f . x = g . x ) assume A14: x in dom F ; ::_thesis: f . x = g . x hence f . x = //\ ((F . x),L) by A11 .= g . x by A12, A14 ; ::_thesis: verum end; ( dom f = dom F & dom g = dom F ) by FUNCT_2:def_1; hence f = g by A13, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines \// WAYBEL_5:def_1_:_ for L being non empty RelStr for F being Function-yielding Function for b3 being Function of (dom F), the carrier of L holds ( b3 = \// (F,L) iff for x being set st x in dom F holds b3 . x = \\/ ((F . x),L) ); :: deftheorem Def2 defines /\\ WAYBEL_5:def_2_:_ for L being non empty RelStr for F being Function-yielding Function for b3 being Function of (dom F), the carrier of L holds ( b3 = /\\ (F,L) iff for x being set st x in dom F holds b3 . x = //\ ((F . x),L) ); notation let J be set ; let K be ManySortedSet of J; let L be non empty RelStr ; let F be DoubleIndexedSet of K,L; synonym Sups F for \// (K,J); synonym Infs F for /\\ (K,J); end; notation let I, J be set ; let L be non empty RelStr ; let F be DoubleIndexedSet of I --> J,L; synonym Sups F for \// (J,I); synonym Infs F for /\\ (J,I); end; theorem Th11: :: WAYBEL_5:11 for L being non empty RelStr for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds \\/ ((F . x),L) = \\/ ((G . x),L) ) holds \// (F,L) = \// (G,L) proof let L be non empty RelStr ; ::_thesis: for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds \\/ ((F . x),L) = \\/ ((G . x),L) ) holds \// (F,L) = \// (G,L) let F, G be Function-yielding Function; ::_thesis: ( dom F = dom G & ( for x being set st x in dom F holds \\/ ((F . x),L) = \\/ ((G . x),L) ) implies \// (F,L) = \// (G,L) ) assume that A1: dom F = dom G and A2: for x being set st x in dom F holds \\/ ((F . x),L) = \\/ ((G . x),L) ; ::_thesis: \// (F,L) = \// (G,L) A3: for x being set st x in dom F holds (\// (F,L)) . x = (\// (G,L)) . x proof let x be set ; ::_thesis: ( x in dom F implies (\// (F,L)) . x = (\// (G,L)) . x ) assume A4: x in dom F ; ::_thesis: (\// (F,L)) . x = (\// (G,L)) . x hence (\// (F,L)) . x = \\/ ((F . x),L) by Def1 .= \\/ ((G . x),L) by A2, A4 .= (\// (G,L)) . x by A1, A4, Def1 ; ::_thesis: verum end; ( dom (\// (F,L)) = dom F & dom (\// (G,L)) = dom G ) by FUNCT_2:def_1; hence \// (F,L) = \// (G,L) by A1, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th12: :: WAYBEL_5:12 for L being non empty RelStr for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds //\ ((F . x),L) = //\ ((G . x),L) ) holds /\\ (F,L) = /\\ (G,L) proof let L be non empty RelStr ; ::_thesis: for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds //\ ((F . x),L) = //\ ((G . x),L) ) holds /\\ (F,L) = /\\ (G,L) let F, G be Function-yielding Function; ::_thesis: ( dom F = dom G & ( for x being set st x in dom F holds //\ ((F . x),L) = //\ ((G . x),L) ) implies /\\ (F,L) = /\\ (G,L) ) assume that A1: dom F = dom G and A2: for x being set st x in dom F holds //\ ((F . x),L) = //\ ((G . x),L) ; ::_thesis: /\\ (F,L) = /\\ (G,L) A3: for x being set st x in dom F holds (/\\ (F,L)) . x = (/\\ (G,L)) . x proof let x be set ; ::_thesis: ( x in dom F implies (/\\ (F,L)) . x = (/\\ (G,L)) . x ) assume A4: x in dom F ; ::_thesis: (/\\ (F,L)) . x = (/\\ (G,L)) . x hence (/\\ (F,L)) . x = //\ ((F . x),L) by Def2 .= //\ ((G . x),L) by A2, A4 .= (/\\ (G,L)) . x by A1, A4, Def2 ; ::_thesis: verum end; ( dom (/\\ (F,L)) = dom F & dom (/\\ (G,L)) = dom G ) by FUNCT_2:def_1; hence /\\ (F,L) = /\\ (G,L) by A1, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th13: :: WAYBEL_5:13 for y being set for L being non empty RelStr for F being Function-yielding Function holds ( ( y in rng (\// (F,L)) implies ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) ) proof let y be set ; ::_thesis: for L being non empty RelStr for F being Function-yielding Function holds ( ( y in rng (\// (F,L)) implies ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) ) let L be non empty RelStr ; ::_thesis: for F being Function-yielding Function holds ( ( y in rng (\// (F,L)) implies ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) ) let F be Function-yielding Function; ::_thesis: ( ( y in rng (\// (F,L)) implies ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being set st ( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) ) thus ( y in rng (\// (F,L)) iff ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) ) ::_thesis: ( y in rng (/\\ (F,L)) iff ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) proof hereby ::_thesis: ( ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) assume y in rng (\// (F,L)) ; ::_thesis: ex x being set st ( x in dom F & y = \\/ ((F . x),L) ) then consider x being set such that A1: ( x in dom (\// (F,L)) & y = (\// (F,L)) . x ) by FUNCT_1:def_3; take x = x; ::_thesis: ( x in dom F & y = \\/ ((F . x),L) ) thus ( x in dom F & y = \\/ ((F . x),L) ) by A1, Def1; ::_thesis: verum end; given x being set such that A2: ( x in dom F & y = \\/ ((F . x),L) ) ; ::_thesis: y in rng (\// (F,L)) ( x in dom (\// (F,L)) & y = (\// (F,L)) . x ) by A2, Def1, FUNCT_2:def_1; hence y in rng (\// (F,L)) by FUNCT_1:def_3; ::_thesis: verum end; thus ( y in rng (/\\ (F,L)) iff ex x being set st ( x in dom F & y = //\ ((F . x),L) ) ) ::_thesis: verum proof hereby ::_thesis: ( ex x being set st ( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) assume y in rng (/\\ (F,L)) ; ::_thesis: ex x being set st ( x in dom F & y = //\ ((F . x),L) ) then consider x being set such that A3: ( x in dom (/\\ (F,L)) & y = (/\\ (F,L)) . x ) by FUNCT_1:def_3; take x = x; ::_thesis: ( x in dom F & y = //\ ((F . x),L) ) thus ( x in dom F & y = //\ ((F . x),L) ) by A3, Def2; ::_thesis: verum end; given x being set such that A4: ( x in dom F & y = //\ ((F . x),L) ) ; ::_thesis: y in rng (/\\ (F,L)) ( x in dom (/\\ (F,L)) & y = (/\\ (F,L)) . x ) by A4, Def2, FUNCT_2:def_1; hence y in rng (/\\ (F,L)) by FUNCT_1:def_3; ::_thesis: verum end; end; theorem Th14: :: WAYBEL_5:14 for x being set for L being non empty RelStr for J being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,L holds ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) proof let x be set ; ::_thesis: for L being non empty RelStr for J being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,L holds ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) let L be non empty RelStr ; ::_thesis: for J being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,L holds ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) let J be non empty set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,L holds ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L holds ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) let F be DoubleIndexedSet of K,L; ::_thesis: ( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) ) A1: dom F = J by PARTFUN1:def_2; thus ( x in rng (Sups ) iff ex j being Element of J st x = Sup ) ::_thesis: ( x in rng (Infs ) iff ex j being Element of J st x = Inf ) proof hereby ::_thesis: ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) assume x in rng (Sups ) ; ::_thesis: ex j being Element of J st x = Sup then consider j being set such that A2: j in dom F and A3: x = \\/ ((F . j),L) by Th13; reconsider j = j as Element of J by A2; take j = j; ::_thesis: x = Sup thus x = Sup by A3; ::_thesis: verum end; thus ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) by A1, Th13; ::_thesis: verum end; hereby ::_thesis: ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) assume x in rng (Infs ) ; ::_thesis: ex j being Element of J st x = Inf then consider j being set such that A4: j in dom F and A5: x = //\ ((F . j),L) by Th13; reconsider j = j as Element of J by A4; take j = j; ::_thesis: x = Inf thus x = Inf by A5; ::_thesis: verum end; thus ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) by A1, Th13; ::_thesis: verum end; registration let J be non empty set ; let K be ManySortedSet of J; let L be non empty RelStr ; let F be DoubleIndexedSet of K,L; cluster proj2 (Sups ) -> non empty ; correctness coherence not rng (Sups ) is empty ; ; cluster proj2 (Infs ) -> non empty ; correctness coherence not rng (Infs ) is empty ; ; end; Lm7: for L being complete LATTICE for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L for f being set holds ( f is Element of product (doms F) iff f in dom (Frege F) ) proof let L be complete LATTICE; ::_thesis: for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L for f being set holds ( f is Element of product (doms F) iff f in dom (Frege F) ) let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L for f being set holds ( f is Element of product (doms F) iff f in dom (Frege F) ) let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L for f being set holds ( f is Element of product (doms F) iff f in dom (Frege F) ) let F be DoubleIndexedSet of K,L; ::_thesis: for f being set holds ( f is Element of product (doms F) iff f in dom (Frege F) ) let f be set ; ::_thesis: ( f is Element of product (doms F) iff f in dom (Frege F) ) hereby ::_thesis: ( f in dom (Frege F) implies f is Element of product (doms F) ) assume f is Element of product (doms F) ; ::_thesis: f in dom (Frege F) then f in product (doms F) ; hence f in dom (Frege F) by PARTFUN1:def_2; ::_thesis: verum end; thus ( f in dom (Frege F) implies f is Element of product (doms F) ) ; ::_thesis: verum end; theorem Th15: :: WAYBEL_5:15 for L being complete LATTICE for a being Element of L for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= a ) holds Sup <= a proof let L be complete LATTICE; ::_thesis: for a being Element of L for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= a ) holds Sup <= a let a be Element of L; ::_thesis: for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= a ) holds Sup <= a let F be Function-yielding Function; ::_thesis: ( ( for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= a ) implies Sup <= a ) assume A1: for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= a ; ::_thesis: Sup <= a rng (/\\ ((Frege F),L)) is_<=_than a proof let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in rng (/\\ ((Frege F),L)) or c <= a ) assume c in rng (/\\ ((Frege F),L)) ; ::_thesis: c <= a then consider f being set such that A2: f in dom (Frege F) and A3: c = //\ (((Frege F) . f),L) by Th13; reconsider f = f as Function by A2; f in dom (Frege F) by A2; hence c <= a by A1, A3; ::_thesis: verum end; then sup (rng (/\\ ((Frege F),L))) <= a by YELLOW_0:32; hence Sup <= a by YELLOW_2:def_5; ::_thesis: verum end; theorem Th16: :: WAYBEL_5:16 for L being complete LATTICE for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf >= Sup proof let L be complete LATTICE; ::_thesis: for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf >= Sup let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf >= Sup let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L holds Inf >= Sup let F be DoubleIndexedSet of K,L; ::_thesis: Inf >= Sup set a = Sup ; A1: for j being Element of J for f being Element of product (doms F) holds Sup >= Inf proof let j be Element of J; ::_thesis: for f being Element of product (doms F) holds Sup >= Inf let f be Element of product (doms F); ::_thesis: Sup >= Inf A2: f in dom (Frege F) by Lm7; then reconsider k = f . j as Element of K . j by Lm6; (F . j) . k = ((Frege F) . f) . j by A2, Lm5; then A3: Inf <= (F . j) . k by YELLOW_2:53; (F . j) . k <= Sup by YELLOW_2:53; hence Sup >= Inf by A3, ORDERS_2:3; ::_thesis: verum end; Sup is_<=_than rng (Sups ) proof let c be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not c in rng (Sups ) or Sup <= c ) assume c in rng (Sups ) ; ::_thesis: Sup <= c then consider j being Element of J such that A4: c = Sup by Th14; for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= c by A1, A4; hence Sup <= c by Th15; ::_thesis: verum end; then Sup <= inf (rng (Sups )) by YELLOW_0:33; hence Inf >= Sup by YELLOW_2:def_6; ::_thesis: verum end; theorem Th17: :: WAYBEL_5:17 for L being complete LATTICE for a, b being Element of L st L is continuous & ( for c being Element of L st c << a holds c <= b ) holds a <= b proof let L be complete LATTICE; ::_thesis: for a, b being Element of L st L is continuous & ( for c being Element of L st c << a holds c <= b ) holds a <= b let a, b be Element of L; ::_thesis: ( L is continuous & ( for c being Element of L st c << a holds c <= b ) implies a <= b ) assume that A1: L is continuous and A2: for c being Element of L st c << a holds c <= b ; ::_thesis: a <= b now__::_thesis:_for_c_being_Element_of_L_st_c_in_waybelow_a_holds_ c_<=_b let c be Element of L; ::_thesis: ( c in waybelow a implies c <= b ) assume c in waybelow a ; ::_thesis: c <= b then c << a by WAYBEL_3:7; hence c <= b by A2; ::_thesis: verum end; then waybelow a is_<=_than b by LATTICE3:def_9; then sup (waybelow a) <= b by YELLOW_0:32; hence a <= b by A1, WAYBEL_3:def_5; ::_thesis: verum end; Lm8: for L being complete LATTICE st L is continuous holds for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup proof let L be complete LATTICE; ::_thesis: ( L is continuous implies for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) assume A1: L is continuous ; ::_thesis: for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup ) assume A2: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup now__::_thesis:_for_c_being_Element_of_L_st_c_<<_Inf_holds_ c_<=_Sup let c be Element of L; ::_thesis: ( c << Inf implies c <= Sup ) assume A3: c << Inf ; ::_thesis: c <= Sup A4: for j being Element of J holds c << Sup proof let j be Element of J; ::_thesis: c << Sup Sup in rng (Sups ) by Th14; then inf (rng (Sups )) <= Sup by YELLOW_2:22; then Inf <= Sup by YELLOW_2:def_6; hence c << Sup by A3, WAYBEL_3:2; ::_thesis: verum end; ex f being Function st ( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st ( b = (F . j) . (f . j) & c <= b ) ) ) proof defpred S1[ set , set ] means ( \$1 in J & \$2 in K . \$1 & ex b being Element of L st ( b = (F . \$1) . \$2 & c <= b ) ); A5: for j being Element of J ex k being Element of K . j st c <= (F . j) . k proof let j be Element of J; ::_thesis: ex k being Element of K . j st c <= (F . j) . k A6: Sup <= sup (rng (F . j)) by YELLOW_2:def_5; ( rng (F . j) is non empty directed Subset of L & c << Sup ) by A2, A4; then consider d being Element of L such that A7: d in rng (F . j) and A8: c <= d by A6, WAYBEL_3:def_1; consider k being set such that A9: k in dom (F . j) and A10: d = (F . j) . k by A7, FUNCT_1:def_3; reconsider k = k as Element of K . j by A9; take k ; ::_thesis: c <= (F . j) . k thus c <= (F . j) . k by A8, A10; ::_thesis: verum end; A11: for j being set st j in J holds ex k being set st ( k in union (rng K) & S1[j,k] ) proof let j be set ; ::_thesis: ( j in J implies ex k being set st ( k in union (rng K) & S1[j,k] ) ) assume j in J ; ::_thesis: ex k being set st ( k in union (rng K) & S1[j,k] ) then reconsider j9 = j as Element of J ; consider k being Element of K . j9 such that A12: c <= (F . j9) . k by A5; take k ; ::_thesis: ( k in union (rng K) & S1[j,k] ) j9 in J ; then j9 in dom K by PARTFUN1:def_2; then K . j9 in rng K by FUNCT_1:def_3; hence k in union (rng K) by TARSKI:def_4; ::_thesis: S1[j,k] thus S1[j,k] by A12; ::_thesis: verum end; consider f being Function such that A13: dom f = J and rng f c= union (rng K) and A14: for j being set st j in J holds S1[j,f . j] from FUNCT_1:sch_5(A11); A15: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_F)_holds_ f_._x_in_(doms_F)_._x let x be set ; ::_thesis: ( x in dom (doms F) implies f . x in (doms F) . x ) assume x in dom (doms F) ; ::_thesis: f . x in (doms F) . x then A16: x in dom F by FUNCT_6:59; then reconsider j = x as Element of J ; (doms F) . x = dom (F . j) by A16, FUNCT_6:22 .= K . j by FUNCT_2:def_1 ; hence f . x in (doms F) . x by A14; ::_thesis: verum end; dom f = dom F by A13, PARTFUN1:def_2 .= dom (doms F) by FUNCT_6:59 ; then f in product (doms F) by A15, CARD_3:9; then A17: f in dom (Frege F) by PARTFUN1:def_2; for j being Element of J holds ( f . j in K . j & ex b being Element of L st ( b = (F . j) . (f . j) & c <= b ) ) by A14; hence ex f being Function st ( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st ( b = (F . j) . (f . j) & c <= b ) ) ) by A17; ::_thesis: verum end; then consider f being Function such that A18: f in dom (Frege F) and A19: for j being Element of J ex b being Element of L st ( b = (F . j) . (f . j) & c <= b ) ; reconsider f = f as Element of product (doms F) by A18; reconsider G = (Frege F) . f as Function of J, the carrier of L ; now__::_thesis:_for_j_being_Element_of_J_holds_c_<=_G_._j let j be Element of J; ::_thesis: c <= G . j j in J ; then A20: j in dom F by PARTFUN1:def_2; ex b being Element of L st ( b = (F . j) . (f . j) & c <= b ) by A19; hence c <= G . j by A18, A20, Th9; ::_thesis: verum end; then A21: c <= Inf by YELLOW_2:55; set a = Inf ; Inf in rng (Infs ) by Th14; then Inf <= sup (rng (Infs )) by YELLOW_2:22; then Inf <= Sup by YELLOW_2:def_5; hence c <= Sup by A21, YELLOW_0:def_2; ::_thesis: verum end; then A22: Inf <= Sup by A1, Th17; Inf >= Sup by Th16; hence Inf = Sup by A22, YELLOW_0:def_3; ::_thesis: verum end; theorem Th18: :: WAYBEL_5:18 for L being complete LATTICE st ( for J being non empty set st J in the_universe_of the carrier of L holds for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) holds L is continuous proof let L be complete LATTICE; ::_thesis: ( ( for J being non empty set st J in the_universe_of the carrier of L holds for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) implies L is continuous ) assume A1: for J being non empty set st J in the_universe_of the carrier of L holds for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ; ::_thesis: L is continuous now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x) set UN = the_universe_of the carrier of L; let x be Element of L; ::_thesis: x = sup (waybelow x) set J = { j where j is non empty directed Subset of L : x <= sup j } ; A2: the_universe_of the carrier of L = Tarski-Class (the_transitive-closure_of the carrier of L) by YELLOW_6:def_1; reconsider UN = the_universe_of the carrier of L as universal set ; A3: { j where j is non empty directed Subset of L : x <= sup j } c= bool the carrier of L proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { j where j is non empty directed Subset of L : x <= sup j } or u in bool the carrier of L ) assume u in { j where j is non empty directed Subset of L : x <= sup j } ; ::_thesis: u in bool the carrier of L then ex j being non empty directed Subset of L st ( u = j & x <= sup j ) ; hence u in bool the carrier of L ; ::_thesis: verum end; ( the carrier of L c= the_transitive-closure_of the carrier of L & the_transitive-closure_of the carrier of L in UN ) by A2, CLASSES1:2, CLASSES1:52; then A4: the carrier of L in UN by CLASSES1:def_1; then bool the carrier of L in UN by CLASSES2:59; then A5: { j where j is non empty directed Subset of L : x <= sup j } in UN by A3, CLASSES1:def_1; x is_>=_than waybelow x by WAYBEL_3:9; then A6: x >= sup (waybelow x) by YELLOW_0:32; ( {x} is non empty directed Subset of L & x <= sup {x} ) by WAYBEL_0:5, YELLOW_0:39; then A7: {x} in { j where j is non empty directed Subset of L : x <= sup j } ; then reconsider J = { j where j is non empty directed Subset of L : x <= sup j } as non empty set ; set K = id J; reconsider K = id J as ManySortedSet of J ; A8: for j being Element of J holds K . j in UN proof let j be Element of J; ::_thesis: K . j in UN K . j = j by FUNCT_1:18; then K . j in J ; hence K . j in UN by A4, A3, CLASSES1:def_1; ::_thesis: verum end; reconsider j = {x} as Element of J by A7; A9: for j being Element of J holds j is non empty directed Subset of L proof let j be Element of J; ::_thesis: j is non empty directed Subset of L j in J ; then ex j9 being non empty directed Subset of L st ( j9 = j & x <= sup j9 ) ; hence j is non empty directed Subset of L ; ::_thesis: verum end; for i being set st i in J holds not K . i is empty proof let i be set ; ::_thesis: ( i in J implies not K . i is empty ) assume i in J ; ::_thesis: not K . i is empty then reconsider i9 = i as Element of J ; K . i = i9 by FUNCT_1:18; hence not K . i is empty by A9; ::_thesis: verum end; then reconsider K = K as V9() ManySortedSet of J by PBOOLE:def_13; deffunc H1( set ) -> Element of bool [:(K . \$1),(K . \$1):] = id (K . \$1); ex F being Function st ( dom F = J & ( for j being set st j in J holds F . j = H1(j) ) ) from FUNCT_1:sch_3(); then consider F being Function such that A10: dom F = J and A11: for j being set st j in J holds F . j = id (K . j) ; reconsider F = F as ManySortedSet of J by A10, PARTFUN1:def_2, RELAT_1:def_18; for j being set st j in dom F holds F . j is Function proof let j be set ; ::_thesis: ( j in dom F implies F . j is Function ) assume j in dom F ; ::_thesis: F . j is Function then F . j = id (K . j) by A11; hence F . j is Function ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def_6; for j being set st j in J holds F . j is Function of (K . j),((J --> the carrier of L) . j) proof let j be set ; ::_thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) ) assume j in J ; ::_thesis: F . j is Function of (K . j),((J --> the carrier of L) . j) then reconsider j = j as Element of J ; K . j = j by FUNCT_1:18; then A12: K . j is Subset of L by A9; A13: F . j = id (K . j) by A11; then rng (F . j) c= K . j by RELAT_1:def_19; then rng (F . j) c= the carrier of L by A12, XBOOLE_1:1; then A14: rng (F . j) c= (J --> the carrier of L) . j by FUNCOP_1:7; dom (F . j) = K . j by A13, FUNCT_2:def_1; hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A14, FUNCT_2:2; ::_thesis: verum end; then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def_15; A15: for j being Element of J for k being Element of K . j holds (F . j) . k = k proof let j be Element of J; ::_thesis: for k being Element of K . j holds (F . j) . k = k let k be Element of K . j; ::_thesis: (F . j) . k = k F . j = id (K . j) by A11; hence (F . j) . k = k by FUNCT_1:18; ::_thesis: verum end; A16: for j being Element of J holds rng (F . j) = j proof let j be Element of J; ::_thesis: rng (F . j) = j now__::_thesis:_for_y_being_set_st_y_in_rng_(F_._j)_holds_ y_in_j let y be set ; ::_thesis: ( y in rng (F . j) implies y in j ) assume y in rng (F . j) ; ::_thesis: y in j then consider x being set such that A17: x in dom (F . j) and A18: y = (F . j) . x by FUNCT_1:def_3; x in K . j by A17; then x in j by FUNCT_1:18; hence y in j by A15, A17, A18; ::_thesis: verum end; then A19: rng (F . j) c= j by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_j_holds_ x_in_rng_(F_._j) let x be set ; ::_thesis: ( x in j implies x in rng (F . j) ) assume x in j ; ::_thesis: x in rng (F . j) then x in K . j by FUNCT_1:18; then ( (F . j) . x = x & x in dom (F . j) ) by A15, FUNCT_2:def_1; hence x in rng (F . j) by FUNCT_1:def_3; ::_thesis: verum end; then j c= rng (F . j) by TARSKI:def_3; hence rng (F . j) = j by A19, XBOOLE_0:def_10; ::_thesis: verum end; A20: for j being Element of J holds rng (F . j) is directed proof let j be Element of J; ::_thesis: rng (F . j) is directed rng (F . j) = j by A16; hence rng (F . j) is directed by A9; ::_thesis: verum end; for f being Function st f in dom (Frege F) holds //\ (((Frege F) . f),L) <= sup (waybelow x) proof let f be Function; ::_thesis: ( f in dom (Frege F) implies //\ (((Frege F) . f),L) <= sup (waybelow x) ) assume A21: f in dom (Frege F) ; ::_thesis: //\ (((Frege F) . f),L) <= sup (waybelow x) set a = //\ (((Frege F) . f),L); for D being non empty directed Subset of L st x <= sup D holds ex d being Element of L st ( d in D & //\ (((Frege F) . f),L) <= d ) proof A22: for j being Element of J holds f . j in K . j proof let j be Element of J; ::_thesis: f . j in K . j j in J ; then j in dom F by PARTFUN1:def_2; then f . j in dom (F . j) by A21, Th9; hence f . j in K . j ; ::_thesis: verum end; A23: dom f = dom F by A21, Th8 .= J by PARTFUN1:def_2 ; now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_the_carrier_of_L let y be set ; ::_thesis: ( y in rng f implies y in the carrier of L ) assume y in rng f ; ::_thesis: y in the carrier of L then consider j being set such that A24: j in dom f and A25: y = f . j by FUNCT_1:def_3; reconsider j = j as Element of J by A23, A24; y in K . j by A22, A25; then A26: y in j by FUNCT_1:18; j is Subset of L by A9; hence y in the carrier of L by A26; ::_thesis: verum end; then rng f c= the carrier of L by TARSKI:def_3; then reconsider f = f as Function of J, the carrier of L by A23, FUNCT_2:2; let D be non empty directed Subset of L; ::_thesis: ( x <= sup D implies ex d being Element of L st ( d in D & //\ (((Frege F) . f),L) <= d ) ) assume x <= sup D ; ::_thesis: ex d being Element of L st ( d in D & //\ (((Frege F) . f),L) <= d ) then D in J ; then reconsider D9 = D as Element of J ; A27: Inf <= f . D9 by YELLOW_2:53; f . D9 in K . D9 by A22; then A28: f . D9 in D9 by FUNCT_1:18; A29: now__::_thesis:_for_j_being_set_st_j_in_dom_f_holds_ ((Frege_F)_._f)_._j_=_f_._j let j be set ; ::_thesis: ( j in dom f implies ((Frege F) . f) . j = f . j ) assume A30: j in dom f ; ::_thesis: ((Frege F) . f) . j = f . j then reconsider j9 = j as Element of J ; A31: f . j9 is Element of K . j9 by A22; j in dom F by A21, A30, Th8; hence ((Frege F) . f) . j = (F . j9) . (f . j9) by A21, Th9 .= f . j by A15, A31 ; ::_thesis: verum end; dom f = dom F by A21, Th8 .= dom ((Frege F) . f) by A21, Th8 ; then //\ (((Frege F) . f),L) <= f . D9 by A27, A29, FUNCT_1:2; hence ex d being Element of L st ( d in D & //\ (((Frege F) . f),L) <= d ) by A28; ::_thesis: verum end; then //\ (((Frege F) . f),L) << x by WAYBEL_3:def_1; then //\ (((Frege F) . f),L) in waybelow x by WAYBEL_3:7; hence //\ (((Frege F) . f),L) <= sup (waybelow x) by YELLOW_2:22; ::_thesis: verum end; then A32: Sup <= sup (waybelow x) by Th15; x is_<=_than rng (Sups ) proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in rng (Sups ) or x <= b ) assume b in rng (Sups ) ; ::_thesis: x <= b then consider j being Element of J such that A33: b = Sup by Th14; j in J ; then consider j9 being non empty directed Subset of L such that A34: j9 = j and A35: x <= sup j9 ; b = sup (rng (F . j)) by A33, YELLOW_2:def_5 .= sup j9 by A16, A34 ; hence x <= b by A35; ::_thesis: verum end; then x <= inf (rng (Sups )) by YELLOW_0:33; then A36: x <= Inf by YELLOW_2:def_6; Sup = sup (rng (F . j)) by YELLOW_2:def_5 .= sup {x} by A16 .= x by YELLOW_0:39 ; then x in rng (Sups ) by Th14; then inf (rng (Sups )) <= x by YELLOW_2:22; then Inf <= x by YELLOW_2:def_6; then x = Inf by A36, ORDERS_2:2 .= Sup by A1, A5, A8, A20 ; hence x = sup (waybelow x) by A32, A6, ORDERS_2:2; ::_thesis: verum end; then ( L is up-complete & L is satisfying_axiom_of_approximation ) by WAYBEL_3:def_5; hence L is continuous ; ::_thesis: verum end; Lm9: for L being complete LATTICE st ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) holds L is continuous proof let L be complete LATTICE; ::_thesis: ( ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) implies L is continuous ) assume for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ; ::_thesis: L is continuous then for J being non empty set st J in the_universe_of the carrier of L holds for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ; hence L is continuous by Th18; ::_thesis: verum end; theorem :: WAYBEL_5:19 for L being complete LATTICE holds ( L is continuous iff for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup ) by Lm8, Lm9; definition let J, K, D be non empty set ; let F be Function of [:J,K:],D; :: original: curry redefine func curry F -> DoubleIndexedSet of J --> K,D; coherence curry F is DoubleIndexedSet of J --> K,D proof reconsider F9 = F as ManySortedSet of [:J,K:] ; A1: dom F = [:J,K:] by FUNCT_2:def_1; for j being set st j in J holds (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) proof let j be set ; ::_thesis: ( j in J implies (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) ) assume A2: j in J ; ::_thesis: (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) then consider g being Function such that A3: (curry F9) . j = g and A4: dom g = K and A5: rng g c= rng F9 and for k being set st k in K holds g . k = F9 . (j,k) by A1, FUNCT_5:29; J = dom (curry F) by A1, FUNCT_5:24; then reconsider G = (curry F9) . j as Function ; rng F c= D ; then rng g c= D by A5, XBOOLE_1:1; then reconsider g = g as Function of K,D by A4, FUNCT_2:def_1, RELSET_1:4; A6: G = g by A3; (J --> K) . j = K by A2, FUNCOP_1:7; hence (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) by A2, A6, FUNCOP_1:7; ::_thesis: verum end; hence curry F is DoubleIndexedSet of J --> K,D by PBOOLE:def_15; ::_thesis: verum end; end; theorem Th20: :: WAYBEL_5:20 for J, K, D being non empty set for j being Element of J for k being Element of K for F being Function of [:J,K:],D holds ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) proof let J, K, D be non empty set ; ::_thesis: for j being Element of J for k being Element of K for F being Function of [:J,K:],D holds ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) let j be Element of J; ::_thesis: for k being Element of K for F being Function of [:J,K:],D holds ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) let k be Element of K; ::_thesis: for F being Function of [:J,K:],D holds ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) let F be Function of [:J,K:],D; ::_thesis: ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) thus dom (curry F) = proj1 (dom F) by FUNCT_5:def_1 .= proj1 [:J,K:] by FUNCT_2:def_1 .= J by FUNCT_5:9 ; ::_thesis: ( dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k ) dom F = [:J,K:] by FUNCT_2:def_1; then ex g being Function st ( (curry F) . j = g & dom g = K & rng g c= rng F & ( for i being set st i in K holds g . i = F . (j,i) ) ) by FUNCT_5:29; hence dom ((curry F) . j) = K ; ::_thesis: F . (j,k) = ((curry F) . j) . k [j,k] in [:J,K:] ; then [j,k] in dom F by FUNCT_2:def_1; hence F . (j,k) = ((curry F) . j) . k by FUNCT_5:20; ::_thesis: verum end; Lm10: for L being complete LATTICE st ( for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup ) holds L is continuous proof let L be complete LATTICE; ::_thesis: ( ( for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup ) implies L is continuous ) assume A1: for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup ; ::_thesis: L is continuous for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup proof let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup ) set j = the Element of J; set k = the Element of K . the Element of J; defpred S1[ set , set , set ] means ( \$1 in J & ( ( \$2 in K . \$1 & \$3 = (F . \$1) . \$2 ) or ( not \$2 in K . \$1 & \$3 = Bottom L ) ) ); A2: dom (doms F) = dom F by FUNCT_6:59; the Element of J in J ; then the Element of J in dom K by PARTFUN1:def_2; then ( the Element of K . the Element of J in K . the Element of J & K . the Element of J in rng K ) by FUNCT_1:def_3; then reconsider K9 = union (rng K) as non empty set by TARSKI:def_4; A3: dom F = J by PARTFUN1:def_2; A4: for j being Element of J for k9 being Element of K9 ex z being Element of L st S1[j,k9,z] proof let j be Element of J; ::_thesis: for k9 being Element of K9 ex z being Element of L st S1[j,k9,z] let k9 be Element of K9; ::_thesis: ex z being Element of L st S1[j,k9,z] percases ( k9 in K . j or not k9 in K . j ) ; suppose k9 in K . j ; ::_thesis: ex z being Element of L st S1[j,k9,z] then reconsider k = k9 as Element of K . j ; take (F . j) . k ; ::_thesis: S1[j,k9,(F . j) . k] thus S1[j,k9,(F . j) . k] ; ::_thesis: verum end; supposeA5: not k9 in K . j ; ::_thesis: ex z being Element of L st S1[j,k9,z] take Bottom L ; ::_thesis: S1[j,k9, Bottom L] thus S1[j,k9, Bottom L] by A5; ::_thesis: verum end; end; end; ex G being Function of [:J,K9:], the carrier of L st for j being Element of J for k being Element of K9 holds S1[j,k,G . (j,k)] from BINOP_1:sch_3(A4); then consider G being Function of [:J,K9:], the carrier of L such that A6: for j being Element of J for k being Element of K9 holds S1[j,k,G . (j,k)] ; A7: for j being Element of J holds K . j c= K9 proof let j be Element of J; ::_thesis: K . j c= K9 hereby :: according to TARSKI:def_3 ::_thesis: verum let k be set ; ::_thesis: ( k in K . j implies k in K9 ) j in J ; then j in dom K by PARTFUN1:def_2; then A8: K . j in rng K by FUNCT_1:def_3; assume k in K . j ; ::_thesis: k in K9 hence k in K9 by A8, TARSKI:def_4; ::_thesis: verum end; end; A9: for j being Element of J holds rng (F . j) c= rng ((curry G) . j) proof let j be Element of J; ::_thesis: rng (F . j) c= rng ((curry G) . j) hereby :: according to TARSKI:def_3 ::_thesis: verum let y be set ; ::_thesis: ( y in rng (F . j) implies y in rng ((curry G) . j) ) assume y in rng (F . j) ; ::_thesis: y in rng ((curry G) . j) then consider k being set such that A10: k in dom (F . j) and A11: y = (F . j) . k by FUNCT_1:def_3; A12: k in K . j by A10; K . j c= K9 by A7; then reconsider k = k as Element of K9 by A12; [j,k] in [:J,K9:] ; then A13: [j,k] in dom G by FUNCT_2:def_1; ( k in K9 & dom ((curry G) . j) = (J --> K9) . j ) by FUNCT_2:def_1; then A14: k in dom ((curry G) . j) by FUNCOP_1:7; y = G . (j,k) by A6, A10, A11 .= ((curry G) . j) . k by A13, FUNCT_5:20 ; hence y in rng ((curry G) . j) by A14, FUNCT_1:def_3; ::_thesis: verum end; end; A15: for j being set st j in dom F holds \\/ ((F . j),L) = \\/ (((curry G) . j),L) proof let j9 be set ; ::_thesis: ( j9 in dom F implies \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) ) assume j9 in dom F ; ::_thesis: \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) then reconsider j = j9 as Element of J ; reconsider H = (curry G) . j as Function of ((J --> K9) . j), the carrier of L ; (J --> K9) . j = K9 by FUNCOP_1:7; then reconsider H = H as Function of K9, the carrier of L ; for k being Element of K9 holds H . k <= Sup proof let k be Element of K9; ::_thesis: H . k <= Sup percases ( k in K . j or not k in K . j ) ; supposeA16: k in K . j ; ::_thesis: H . k <= Sup then A17: k in dom (F . j) by FUNCT_2:def_1; (F . j) . k = G . (j,k) by A6, A16 .= H . k by Th20 ; then H . k in rng (F . j) by A17, FUNCT_1:def_3; then H . k <= sup (rng (F . j)) by YELLOW_2:22; hence H . k <= Sup by YELLOW_2:def_5; ::_thesis: verum end; suppose not k in K . j ; ::_thesis: H . k <= Sup then Bottom L = G . (j,k) by A6 .= H . k by Th20 ; hence H . k <= Sup by YELLOW_0:44; ::_thesis: verum end; end; end; then A18: Sup <= Sup by YELLOW_2:54; ( ex_sup_of rng (F . j),L & ex_sup_of rng ((curry G) . j),L ) by YELLOW_0:17; then sup (rng (F . j)) <= sup (rng ((curry G) . j)) by A9, YELLOW_0:34; then Sup <= sup (rng H) by YELLOW_2:def_5; then Sup <= Sup by YELLOW_2:def_5; hence \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) by A18, ORDERS_2:2; ::_thesis: verum end; A19: dom (doms (curry G)) = dom (curry G) by FUNCT_6:59; A20: dom (curry G) = J by Th20; product (doms F) c= product (doms (curry G)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (doms F) or x in product (doms (curry G)) ) assume x in product (doms F) ; ::_thesis: x in product (doms (curry G)) then consider g being Function such that A21: x = g and A22: dom g = dom (doms F) and A23: for j being set st j in dom (doms F) holds g . j in (doms F) . j by CARD_3:def_5; A24: for j being set st j in dom (doms (curry G)) holds g . j in (doms (curry G)) . j proof let j be set ; ::_thesis: ( j in dom (doms (curry G)) implies g . j in (doms (curry G)) . j ) assume A25: j in dom (doms (curry G)) ; ::_thesis: g . j in (doms (curry G)) . j then reconsider j9 = j as Element of J by A19; j in J by A19, A25; then A26: g . j in (doms F) . j by A2, A3, A23; A27: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22 .= K . j9 by FUNCT_2:def_1 ; A28: K . j9 c= K9 by A7; (doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22 .= K9 by Th20 ; hence g . j in (doms (curry G)) . j by A26, A27, A28; ::_thesis: verum end; dom g = dom (doms (curry G)) by A2, A3, A19, A22, Th20; hence x in product (doms (curry G)) by A21, A24, CARD_3:def_5; ::_thesis: verum end; then dom (Frege F) c= product (doms (curry G)) by PARTFUN1:def_2; then A29: dom (Frege F) c= dom (Frege (curry G)) by PARTFUN1:def_2; A30: for f being set st f in dom (Frege F) holds //\ (((Frege F) . f),L) = //\ (((Frege (curry G)) . f),L) proof let f9 be set ; ::_thesis: ( f9 in dom (Frege F) implies //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) ) assume A31: f9 in dom (Frege F) ; ::_thesis: //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) then reconsider f = f9 as Element of product (doms F) ; A32: dom ((Frege F) . f) = dom F by A31, Th8 .= J by PARTFUN1:def_2 ; A33: for j being set st j in J holds ((Frege F) . f) . j = ((Frege (curry G)) . f) . j proof let j9 be set ; ::_thesis: ( j9 in J implies ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 ) assume j9 in J ; ::_thesis: ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 then reconsider j = j9 as Element of J ; A34: f . j in K . j by A31, Lm6; K . j c= K9 by A7; then reconsider fj = f . j as Element of K9 by A34; ((Frege F) . f) . j = (F . j) . fj by A31, Lm5 .= G . (j,fj) by A6, A34 .= ((curry G) . j) . (f . j) by Th20 .= ((Frege (curry G)) . f) . j by A29, A31, Lm5 ; hence ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 ; ::_thesis: verum end; dom ((Frege (curry G)) . f) = dom (curry G) by A29, A31, Th8 .= proj1 (dom G) by FUNCT_5:def_1 .= proj1 [:J,K9:] by FUNCT_2:def_1 .= J by FUNCT_5:9 ; hence //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) by A32, A33, FUNCT_1:2; ::_thesis: verum end; A35: Sup = Sup proof percases ( for j being Element of J holds K . j = K9 or ex j being Element of J st K . j <> K9 ) ; supposeA36: for j being Element of J holds K . j = K9 ; ::_thesis: Sup = Sup for j being set st j in J holds (doms F) . j = (doms (curry G)) . j proof let j be set ; ::_thesis: ( j in J implies (doms F) . j = (doms (curry G)) . j ) assume j in J ; ::_thesis: (doms F) . j = (doms (curry G)) . j then reconsider j9 = j as Element of J ; A37: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22 .= K . j9 by FUNCT_2:def_1 ; (doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22 .= K9 by Th20 ; hence (doms F) . j = (doms (curry G)) . j by A36, A37; ::_thesis: verum end; then doms F = doms (curry G) by A2, A3, A19, A20, FUNCT_1:2; then dom (Frege F) = product (doms (curry G)) by PARTFUN1:def_2; then dom (Frege F) = dom (Frege (curry G)) by PARTFUN1:def_2; hence Sup = Sup by A30, Th12; ::_thesis: verum end; suppose ex j being Element of J st K . j <> K9 ; ::_thesis: Sup = Sup then consider j being Element of J such that A38: K . j <> K9 ; K . j c= K9 by A7; then not K9 c= K . j by A38, XBOOLE_0:def_10; then consider k being set such that A39: k in K9 and A40: not k in K . j by TARSKI:def_3; reconsider k = k as Element of K9 by A39; A41: (rng (Infs )) \/ {(Bottom L)} c= rng (Infs ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng (Infs )) \/ {(Bottom L)} or x in rng (Infs ) ) assume A42: x in (rng (Infs )) \/ {(Bottom L)} ; ::_thesis: x in rng (Infs ) percases ( x in rng (Infs ) or x in {(Bottom L)} ) by A42, XBOOLE_0:def_3; suppose x in rng (Infs ) ; ::_thesis: x in rng (Infs ) then consider f being set such that A43: f in dom (Frege F) and A44: x = //\ (((Frege F) . f),L) by Th13; x = //\ (((Frege (curry G)) . f),L) by A30, A43, A44; hence x in rng (Infs ) by A29, A43, Th13; ::_thesis: verum end; supposeA45: x in {(Bottom L)} ; ::_thesis: x in rng (Infs ) then reconsider x9 = x as Element of L ; set f = J --> k; A46: for x being set st x in dom (doms (curry G)) holds (J --> k) . x in (doms (curry G)) . x proof let x be set ; ::_thesis: ( x in dom (doms (curry G)) implies (J --> k) . x in (doms (curry G)) . x ) assume x in dom (doms (curry G)) ; ::_thesis: (J --> k) . x in (doms (curry G)) . x then reconsider j = x as Element of J by A19; A47: (J --> k) . j = k by FUNCOP_1:7; (doms (curry G)) . j = dom ((curry G) . j) by A20, FUNCT_6:22 .= K9 by Th20 ; hence (J --> k) . x in (doms (curry G)) . x by A47; ::_thesis: verum end; dom (J --> k) = J by FUNCOP_1:13 .= dom (doms (curry G)) by A19, Th20 ; then J --> k in product (doms (curry G)) by A46, CARD_3:9; then A48: J --> k in dom (Frege (curry G)) by PARTFUN1:def_2; A49: x = Bottom L by A45, TARSKI:def_1; then x = G . (j,k) by A6, A40 .= ((curry G) . j) . k by Th20 .= ((curry G) . j) . ((J --> k) . j) by FUNCOP_1:7 ; then x in rng ((Frege (curry G)) . (J --> k)) by A48, Lm5; then x9 >= "/\" ((rng ((Frege (curry G)) . (J --> k))),L) by YELLOW_2:22; then A50: x9 >= //\ (((Frege (curry G)) . (J --> k)),L) by YELLOW_2:def_6; x9 <= //\ (((Frege (curry G)) . (J --> k)),L) by A49, YELLOW_0:44; then x9 = //\ (((Frege (curry G)) . (J --> k)),L) by A50, ORDERS_2:2; hence x in rng (Infs ) by A48, Th13; ::_thesis: verum end; end; end; A51: ( ex_sup_of rng (Infs ),L & ex_sup_of {(Bottom L)},L ) by YELLOW_0:17; A52: rng (Infs ) c= (rng (Infs )) \/ {(Bottom L)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Infs ) or x in (rng (Infs )) \/ {(Bottom L)} ) assume x in rng (Infs ) ; ::_thesis: x in (rng (Infs )) \/ {(Bottom L)} then consider f being set such that A53: f in dom (Frege (curry G)) and A54: x = //\ (((Frege (curry G)) . f),L) by Th13; reconsider f = f as Function by A53; percases ( for j being Element of J holds f . j in K . j or ex j being Element of J st not f . j in K . j ) ; supposeA55: for j being Element of J holds f . j in K . j ; ::_thesis: x in (rng (Infs )) \/ {(Bottom L)} A56: for x being set st x in dom (doms F) holds f . x in (doms F) . x proof let x be set ; ::_thesis: ( x in dom (doms F) implies f . x in (doms F) . x ) assume x in dom (doms F) ; ::_thesis: f . x in (doms F) . x then reconsider j = x as Element of J by A3, FUNCT_6:59; (doms F) . j = dom (F . j) by A3, FUNCT_6:22 .= K . j by FUNCT_2:def_1 ; hence f . x in (doms F) . x by A55; ::_thesis: verum end; dom f = dom (curry G) by A53, Th8 .= dom (doms F) by A2, A3, Th20 ; then f in product (doms F) by A56, CARD_3:9; then A57: f in dom (Frege F) by PARTFUN1:def_2; then x = //\ (((Frege F) . f),L) by A30, A54; then x in rng (Infs ) by A57, Th13; hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def_3; ::_thesis: verum end; suppose not for j being Element of J holds f . j in K . j ; ::_thesis: x in (rng (Infs )) \/ {(Bottom L)} then consider j being Element of J such that A58: not f . j in K . j ; j in J ; then j in dom (curry G) by Th20; then f . j in dom ((curry G) . j) by A53, Th9; then reconsider k = f . j as Element of K9 by Th20; Bottom L = G . (j,k) by A6, A58 .= ((curry G) . j) . (f . j) by Th20 ; then Bottom L in rng ((Frege (curry G)) . f) by A53, Lm5; then Bottom L >= "/\" ((rng ((Frege (curry G)) . f)),L) by YELLOW_2:22; then A59: Bottom L >= //\ (((Frege (curry G)) . f),L) by YELLOW_2:def_6; Bottom L <= //\ (((Frege (curry G)) . f),L) by YELLOW_0:44; then x = Bottom L by A54, A59, ORDERS_2:2; then x in {(Bottom L)} by TARSKI:def_1; hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def_3; ::_thesis: verum end; end; end; A60: Bottom L <= Sup by YELLOW_0:44; Sup = sup (rng (Infs )) by YELLOW_2:def_5 .= sup ((rng (Infs )) \/ {(Bottom L)}) by A52, A41, XBOOLE_0:def_10 .= (sup (rng (Infs ))) "\/" (sup {(Bottom L)}) by A51, YELLOW_2:3 .= (sup (rng (Infs ))) "\/" (Bottom L) by YELLOW_0:39 .= (Sup ) "\/" (Bottom L) by YELLOW_2:def_5 .= Sup by A60, YELLOW_0:24 ; hence Sup = Sup ; ::_thesis: verum end; end; end; assume A61: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup A62: for j being Element of J holds rng ((curry G) . j) is directed proof let j be Element of J; ::_thesis: rng ((curry G) . j) is directed set X = rng ((curry G) . j); for x, y being Element of L st x in rng ((curry G) . j) & y in rng ((curry G) . j) holds ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) proof A63: rng (F . j) is directed by A61; let x, y be Element of L; ::_thesis: ( x in rng ((curry G) . j) & y in rng ((curry G) . j) implies ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) ) assume that A64: x in rng ((curry G) . j) and A65: y in rng ((curry G) . j) ; ::_thesis: ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) consider b being set such that A66: b in dom ((curry G) . j) and A67: ((curry G) . j) . b = y by A65, FUNCT_1:def_3; consider a being set such that A68: a in dom ((curry G) . j) and A69: ((curry G) . j) . a = x by A64, FUNCT_1:def_3; reconsider a9 = a, b9 = b as Element of K9 by A68, A66, Th20; A70: x = G . (j,a9) by A69, Th20; A71: y = G . (j,b9) by A67, Th20; percases ( ( a in K . j & b in K . j ) or ( a in K . j & not b in K . j ) or ( not a in K . j & b in K . j ) or ( not a in K . j & not b in K . j ) ) ; supposeA72: ( a in K . j & b in K . j ) ; ::_thesis: ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) then ( b in dom (F . j) & y = (F . j) . b9 ) by A6, A71, FUNCT_2:def_1; then A73: y in rng (F . j) by FUNCT_1:def_3; ( a in dom (F . j) & x = (F . j) . a9 ) by A6, A70, A72, FUNCT_2:def_1; then x in rng (F . j) by FUNCT_1:def_3; then consider z being Element of L such that A74: ( z in rng (F . j) & x <= z & y <= z ) by A63, A73, WAYBEL_0:def_1; take z ; ::_thesis: ( z in rng ((curry G) . j) & x <= z & y <= z ) rng (F . j) c= rng ((curry G) . j) by A9; hence ( z in rng ((curry G) . j) & x <= z & y <= z ) by A74; ::_thesis: verum end; supposeA75: ( a in K . j & not b in K . j ) ; ::_thesis: ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) take x ; ::_thesis: ( x in rng ((curry G) . j) & x <= x & y <= x ) y = Bottom L by A6, A71, A75; hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A64, YELLOW_0:44; ::_thesis: verum end; supposeA76: ( not a in K . j & b in K . j ) ; ::_thesis: ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) take y ; ::_thesis: ( y in rng ((curry G) . j) & x <= y & y <= y ) x = Bottom L by A6, A70, A76; hence ( y in rng ((curry G) . j) & x <= y & y <= y ) by A65, YELLOW_0:44; ::_thesis: verum end; supposeA77: ( not a in K . j & not b in K . j ) ; ::_thesis: ex z being Element of L st ( z in rng ((curry G) . j) & x <= z & y <= z ) take x ; ::_thesis: ( x in rng ((curry G) . j) & x <= x & y <= x ) x = Bottom L by A6, A70, A77; hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A6, A64, A71, A77; ::_thesis: verum end; end; end; hence rng ((curry G) . j) is directed by WAYBEL_0:def_1; ::_thesis: verum end; dom F = J by PARTFUN1:def_2 .= dom (curry G) by PARTFUN1:def_2 ; hence Inf = Inf by A15, Th11 .= Sup by A1, A62, A35 ; ::_thesis: verum end; hence L is continuous by Lm9; ::_thesis: verum end; theorem :: WAYBEL_5:21 for L being complete LATTICE holds ( L is continuous iff for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup ) by Lm8, Lm10; Lm11: for J, K being non empty set for f being Function st f in Funcs (J,(Fin K)) holds for j being Element of J holds f . j is finite Subset of K proof let J, K be non empty set ; ::_thesis: for f being Function st f in Funcs (J,(Fin K)) holds for j being Element of J holds f . j is finite Subset of K let f be Function; ::_thesis: ( f in Funcs (J,(Fin K)) implies for j being Element of J holds f . j is finite Subset of K ) assume f in Funcs (J,(Fin K)) ; ::_thesis: for j being Element of J holds f . j is finite Subset of K then A1: ex f9 being Function st ( f9 = f & dom f9 = J & rng f9 c= Fin K ) by FUNCT_2:def_2; for j being Element of J holds f . j is finite Subset of K proof let j be Element of J; ::_thesis: f . j is finite Subset of K f . j in rng f by A1, FUNCT_1:def_3; hence f . j is finite Subset of K by A1, FINSUB_1:def_5; ::_thesis: verum end; hence for j being Element of J holds f . j is finite Subset of K ; ::_thesis: verum end; Lm12: for L being complete LATTICE for J, K, D being non empty set for j being Element of J for F being Function of [:J,K:],D for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) proof let L be complete LATTICE; ::_thesis: for J, K, D being non empty set for j being Element of J for F being Function of [:J,K:],D for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) let J, K, D be non empty set ; ::_thesis: for j being Element of J for F being Function of [:J,K:],D for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) let j be Element of J; ::_thesis: for F being Function of [:J,K:],D for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) let F be Function of [:J,K:],D; ::_thesis: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) let f be V9() ManySortedSet of J; ::_thesis: ( f in Funcs (J,(Fin K)) implies for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) ) assume f in Funcs (J,(Fin K)) ; ::_thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds rng (G . j) is finite Subset of (rng ((curry F) . j)) then A1: f . j is finite Subset of K by Lm11; let G be DoubleIndexedSet of f,L; ::_thesis: ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) implies rng (G . j) is finite Subset of (rng ((curry F) . j)) ) assume A2: for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ; ::_thesis: rng (G . j) is finite Subset of (rng ((curry F) . j)) rng (G . j) c= rng ((curry F) . j) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (G . j) or y in rng ((curry F) . j) ) assume y in rng (G . j) ; ::_thesis: y in rng ((curry F) . j) then consider k being set such that A3: k in dom (G . j) and A4: y = (G . j) . k by FUNCT_1:def_3; A5: k in f . j by A3; then A6: k in K by A1; reconsider k = k as Element of K by A1, A5; A7: k in dom ((curry F) . j) by A6, Th20; y = F . (j,k) by A2, A3, A4 .= ((curry F) . j) . k by Th20 ; hence y in rng ((curry F) . j) by A7, FUNCT_1:def_3; ::_thesis: verum end; hence rng (G . j) is finite Subset of (rng ((curry F) . j)) by A1; ::_thesis: verum end; theorem Th22: :: WAYBEL_5:22 for L being complete LATTICE for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf >= sup X proof let L be complete LATTICE; ::_thesis: for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf >= sup X let J, K be non empty set ; ::_thesis: for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf >= sup X let F be Function of [:J,K:], the carrier of L; ::_thesis: for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf >= sup X let X be Subset of L; ::_thesis: ( X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } implies Inf >= sup X ) A1: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds for j being Element of J holds Sup >= Sup proof let f be V9() ManySortedSet of J; ::_thesis: ( f in Funcs (J,(Fin K)) implies for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds for j being Element of J holds Sup >= Sup ) assume A2: f in Funcs (J,(Fin K)) ; ::_thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds for j being Element of J holds Sup >= Sup let G be DoubleIndexedSet of f,L; ::_thesis: ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) implies for j being Element of J holds Sup >= Sup ) assume A3: for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ; ::_thesis: for j being Element of J holds Sup >= Sup let j be Element of J; ::_thesis: Sup >= Sup A4: ( ex_sup_of rng ((curry F) . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17; rng (G . j) is Subset of (rng ((curry F) . j)) by A2, A3, Lm12; then sup (rng ((curry F) . j)) >= sup (rng (G . j)) by A4, YELLOW_0:34; then Sup >= sup (rng (G . j)) by YELLOW_2:def_5; hence Sup >= Sup by YELLOW_2:def_5; ::_thesis: verum end; A5: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds Inf >= Inf proof let f be V9() ManySortedSet of J; ::_thesis: ( f in Funcs (J,(Fin K)) implies for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds Inf >= Inf ) assume A6: f in Funcs (J,(Fin K)) ; ::_thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) holds Inf >= Inf let G be DoubleIndexedSet of f,L; ::_thesis: ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) implies Inf >= Inf ) assume A7: for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ; ::_thesis: Inf >= Inf rng (Sups ) is_>=_than Inf proof let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in rng (Sups ) or Inf <= a ) assume a in rng (Sups ) ; ::_thesis: Inf <= a then consider j being Element of J such that A8: a = Sup by Th14; Sup in rng (Sups ) by Th14; then Sup >= inf (rng (Sups )) by YELLOW_2:22; then A9: Sup >= Inf by YELLOW_2:def_6; Sup >= Sup by A1, A6, A7; hence Inf <= a by A8, A9, ORDERS_2:3; ::_thesis: verum end; then inf (rng (Sups )) >= Inf by YELLOW_0:33; hence Inf >= Inf by YELLOW_2:def_6; ::_thesis: verum end; assume A10: X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } ; ::_thesis: Inf >= sup X Inf is_>=_than X proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <= Inf ) assume a in X ; ::_thesis: a <= Inf then ex a9 being Element of L st ( a9 = a & ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a9 = Inf ) ) ) by A10; hence a <= Inf by A5; ::_thesis: verum end; hence Inf >= sup X by YELLOW_0:32; ::_thesis: verum end; Lm13: for L being complete LATTICE st L is continuous holds for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X proof let L be complete LATTICE; ::_thesis: ( L is continuous implies for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ) assume A1: L is continuous ; ::_thesis: for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X hereby ::_thesis: verum let J, K be non empty set ; ::_thesis: for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X set FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } ; set k = the Element of K; { the Element of K} in { A where A is Subset of K : ( A is finite & A <> {} ) } ; then reconsider FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } as non empty set ; let F be Function of [:J,K:], the carrier of L; ::_thesis: for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X let X be Subset of L; ::_thesis: ( X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } implies Inf = sup X ) set N = Funcs (J,FIK); deffunc H1( Element of J, Element of Funcs (J,FIK)) -> Element of the carrier of L = sup (((curry F) . \$1) .: (\$2 . \$1)); ex H being Function of [:J,(Funcs (J,FIK)):], the carrier of L st for j being Element of J for g being Element of Funcs (J,FIK) holds H . (j,g) = H1(j,g) from BINOP_1:sch_4(); then consider H being Function of [:J,(Funcs (J,FIK)):], the carrier of L such that A2: for j being Element of J for g being Element of Funcs (J,FIK) holds H . (j,g) = sup (((curry F) . j) .: (g . j)) ; set cF = curry F; set cH = curry H; A3: for j being Element of J holds ( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) ) ) proof let j be Element of J; ::_thesis: ( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) ) ) set D = rng ((curry H) . j); set R = rng ((curry F) . j); set Hj = (curry H) . j; set Fj = (curry F) . j; thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds ex_sup_of Y,L by YELLOW_0:17; ::_thesis: ( ( for x being Element of L st x in rng ((curry H) . j) holds ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) ) ) thus for x being Element of L st x in rng ((curry H) . j) holds ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ::_thesis: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) proof let x be Element of L; ::_thesis: ( x in rng ((curry H) . j) implies ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) assume x in rng ((curry H) . j) ; ::_thesis: ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) then consider g being set such that A4: g in dom ((curry H) . j) and A5: ((curry H) . j) . g = x by FUNCT_1:def_3; reconsider g = g as Element of Funcs (J,FIK) by A4, Th20; g . j in FIK ; then ex A being Subset of K st ( A = g . j & A is finite & A <> {} ) ; then reconsider Y = ((curry F) . j) .: (g . j) as finite Subset of (rng ((curry F) . j)) by RELAT_1:111; take Y ; ::_thesis: ( ex_sup_of Y,L & x = "\/" (Y,L) ) x = H . (j,g) by A5, Th20 .= sup (((curry F) . j) .: (g . j)) by A2 ; hence ( ex_sup_of Y,L & x = "\/" (Y,L) ) by YELLOW_0:17; ::_thesis: verum end; thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) ::_thesis: verum proof let Y be finite Subset of (rng ((curry F) . j)); ::_thesis: ( Y <> {} implies "\/" (Y,L) in rng ((curry H) . j) ) consider Z being set such that A6: Z c= dom ((curry F) . j) and A7: Z is finite and A8: ((curry F) . j) .: Z = Y by ORDERS_1:85; A9: Z c= K by A6, Th20; assume Y <> {} ; ::_thesis: "\/" (Y,L) in rng ((curry H) . j) then Z <> {} by A8; then Z in FIK by A7, A9; then A10: {Z} c= FIK by ZFMISC_1:31; ( dom (J --> Z) = J & rng (J --> Z) = {Z} ) by FUNCOP_1:8, FUNCOP_1:13; then reconsider g = J --> Z as Element of Funcs (J,FIK) by A10, FUNCT_2:def_2; A11: g . j = Z by FUNCOP_1:7; g in Funcs (J,FIK) ; then A12: g in dom ((curry H) . j) by Th20; ((curry H) . j) . g = H . (j,g) by Th20 .= "\/" (Y,L) by A2, A8, A11 ; hence "\/" (Y,L) in rng ((curry H) . j) by A12, FUNCT_1:def_3; ::_thesis: verum end; end; for j being Element of J holds rng ((curry H) . j) is directed proof let j be Element of J; ::_thesis: rng ((curry H) . j) is directed A13: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) by A3; ( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) ) by A3; hence rng ((curry H) . j) is directed by A13, WAYBEL_0:51; ::_thesis: verum end; then A14: Inf = Sup by A1, Lm8; A15: for j being set st j in dom (curry F) holds \\/ (((curry F) . j),L) = \\/ (((curry H) . j),L) proof let j9 be set ; ::_thesis: ( j9 in dom (curry F) implies \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) ) assume j9 in dom (curry F) ; ::_thesis: \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) then reconsider j = j9 as Element of J ; A16: ( ( for x being Element of L st x in rng ((curry H) . j) holds ex Y being finite Subset of (rng ((curry F) . j)) st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds "\/" (Y,L) in rng ((curry H) . j) ) ) by A3; ( ex_sup_of rng ((curry F) . j),L & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds ex_sup_of Y,L ) ) by YELLOW_0:17; then sup (rng ((curry F) . j)) = sup (rng ((curry H) . j)) by A16, WAYBEL_0:54; then Sup = sup (rng ((curry H) . j)) by YELLOW_2:def_5; hence \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) by YELLOW_2:def_5; ::_thesis: verum end; assume A17: X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } ; ::_thesis: Inf = sup X then A18: Inf >= sup X by Th22; A19: FIK c= Fin K proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FIK or x in Fin K ) assume x in FIK ; ::_thesis: x in Fin K then ex A being Subset of K st ( x = A & A is finite & A <> {} ) ; hence x in Fin K by FINSUB_1:def_5; ::_thesis: verum end; A20: for h being Function-yielding Function st h in product (doms (curry H)) holds ( ( for j being Element of J holds ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) proof let h be Function-yielding Function; ::_thesis: ( h in product (doms (curry H)) implies ( ( for j being Element of J holds ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) ) set f = (Frege h) . (id J); assume h in product (doms (curry H)) ; ::_thesis: ( ( for j being Element of J holds ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) then A21: h in dom (Frege (curry H)) by PARTFUN1:def_2; then A22: dom h = dom (curry H) by Th8 .= J by Th20 ; A23: for x being set st x in dom (doms h) holds (id J) . x in (doms h) . x proof let x be set ; ::_thesis: ( x in dom (doms h) implies (id J) . x in (doms h) . x ) assume x in dom (doms h) ; ::_thesis: (id J) . x in (doms h) . x then reconsider j = x as Element of J by A22, FUNCT_6:59; h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6; then h . j in Funcs (J,FIK) by FUNCOP_1:7; then ex g being Function st ( g = h . j & dom g = J & rng g c= FIK ) by FUNCT_2:def_2; then ( (id J) . j = j & (doms h) . j = J ) by A22, FUNCT_1:18, FUNCT_6:22; hence (id J) . x in (doms h) . x ; ::_thesis: verum end; ( dom (id J) = J & dom (doms h) = dom h ) by FUNCT_6:59; then id J in product (doms h) by A22, A23, CARD_3:9; then A24: id J in dom (Frege h) by PARTFUN1:def_2; then A25: dom ((Frege h) . (id J)) = J by A22, Th8; then reconsider f9 = (Frege h) . (id J) as ManySortedSet of J by PARTFUN1:def_2, RELAT_1:def_18; thus A26: for j being Element of J holds ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ::_thesis: ( (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) proof let j be Element of J; ::_thesis: ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) thus A27: ((Frege h) . (id J)) . j = (h . j) . ((id J) . j) by A22, A24, Th9 .= (h . j) . j by FUNCT_1:18 ; ::_thesis: ( h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6; hence h . j in Funcs (J,FIK) by FUNCOP_1:7; ::_thesis: ((Frege h) . (id J)) . j is non empty finite Subset of K then consider g being Function such that A28: ( g = h . j & dom g = J ) and A29: rng g c= FIK by FUNCT_2:def_2; ((Frege h) . (id J)) . j in rng g by A27, A28, FUNCT_1:def_3; then ((Frege h) . (id J)) . j in FIK by A29; then ex A being Subset of K st ( ((Frege h) . (id J)) . j = A & A is finite & A <> {} ) ; hence ((Frege h) . (id J)) . j is non empty finite Subset of K ; ::_thesis: verum end; then for j being set st j in J holds not f9 . j is empty ; hence (Frege h) . (id J) is V9() ManySortedSet of J by PBOOLE:def_13; ::_thesis: ( (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) A30: rng ((Frege h) . (id J)) c= FIK proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((Frege h) . (id J)) or y in FIK ) assume y in rng ((Frege h) . (id J)) ; ::_thesis: y in FIK then consider j being set such that A31: j in dom ((Frege h) . (id J)) and A32: y = ((Frege h) . (id J)) . j by FUNCT_1:def_3; ((Frege h) . (id J)) . j is non empty finite Subset of K by A26, A25, A31; hence y in FIK by A32; ::_thesis: verum end; hence (Frege h) . (id J) in Funcs (J,FIK) by A25, FUNCT_2:def_2; ::_thesis: (Frege h) . (id J) in Funcs (J,(Fin K)) rng ((Frege h) . (id J)) c= Fin K by A19, A30, XBOOLE_1:1; hence (Frege h) . (id J) in Funcs (J,(Fin K)) by A25, FUNCT_2:def_2; ::_thesis: verum end; A33: for h being Element of product (doms (curry H)) holds Inf <= sup X proof defpred S1[ set , set , set ] means \$1 = F . (\$3,\$2); let h be Element of product (doms (curry H)); ::_thesis: Inf <= sup X h in product (doms (curry H)) ; then A34: h in dom (Frege (curry H)) by PARTFUN1:def_2; for x being set st x in dom h holds h . x is Function proof let x be set ; ::_thesis: ( x in dom h implies h . x is Function ) assume A35: x in dom h ; ::_thesis: h . x is Function dom h = dom (curry H) by A34, Th8 .= J by Th20 ; then reconsider j = x as Element of J by A35; h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6; then h . j in Funcs (J,FIK) by FUNCOP_1:7; hence h . x is Function ; ::_thesis: verum end; then reconsider h9 = h as Function-yielding Function by FUNCOP_1:def_6; reconsider f = (Frege h9) . (id J) as V9() ManySortedSet of J by A20; A36: for j being set st j in J holds for x being set st x in f . j holds ex y being set st ( y in (J --> the carrier of L) . j & S1[y,x,j] ) proof let i be set ; ::_thesis: ( i in J implies for x being set st x in f . i holds ex y being set st ( y in (J --> the carrier of L) . i & S1[y,x,i] ) ) assume i in J ; ::_thesis: for x being set st x in f . i holds ex y being set st ( y in (J --> the carrier of L) . i & S1[y,x,i] ) then reconsider j = i as Element of J ; let x be set ; ::_thesis: ( x in f . i implies ex y being set st ( y in (J --> the carrier of L) . i & S1[y,x,i] ) ) assume A37: x in f . i ; ::_thesis: ex y being set st ( y in (J --> the carrier of L) . i & S1[y,x,i] ) f . j is Subset of K by A20; then reconsider k = x as Element of K by A37; take y = F . [j,k]; ::_thesis: ( y in (J --> the carrier of L) . i & S1[y,x,i] ) y in the carrier of L ; hence ( y in (J --> the carrier of L) . i & S1[y,x,i] ) by FUNCOP_1:7; ::_thesis: verum end; ex G being ManySortedFunction of f,J --> the carrier of L st for j being set st j in J holds ex g being Function of (f . j),((J --> the carrier of L) . j) st ( g = G . j & ( for x being set st x in f . j holds S1[g . x,x,j] ) ) from MSSUBFAM:sch_1(A36); then consider G being ManySortedFunction of f,J --> the carrier of L such that A38: for j being set st j in J holds ex g being Function of (f . j),((J --> the carrier of L) . j) st ( g = G . j & ( for x being set st x in f . j holds g . x = F . (j,x) ) ) ; reconsider G = G as DoubleIndexedSet of f,L ; A39: for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) proof let j be Element of J; ::_thesis: for x being set st x in f . j holds (G . j) . x = F . (j,x) let x be set ; ::_thesis: ( x in f . j implies (G . j) . x = F . (j,x) ) assume A40: x in f . j ; ::_thesis: (G . j) . x = F . (j,x) ex g being Function of (f . j),((J --> the carrier of L) . j) st ( g = G . j & ( for x being set st x in f . j holds g . x = F . (j,x) ) ) by A38; hence (G . j) . x = F . (j,x) by A40; ::_thesis: verum end; Inf is_<=_than rng (Sups ) proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in rng (Sups ) or Inf <= y ) assume y in rng (Sups ) ; ::_thesis: Inf <= y then consider j being Element of J such that A41: y = Sup by Th14; j in J ; then A42: j in dom (curry H) by Th20; A43: ((curry F) . j) .: (f . j) c= rng (G . j) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((curry F) . j) .: (f . j) or y in rng (G . j) ) assume y in ((curry F) . j) .: (f . j) ; ::_thesis: y in rng (G . j) then consider x being set such that A44: x in dom ((curry F) . j) and A45: x in f . j and A46: y = ((curry F) . j) . x by FUNCT_1:def_6; reconsider k = x as Element of K by A44, Th20; A47: k in dom (G . j) by A45, FUNCT_2:def_1; y = F . (j,k) by A46, Th20 .= (G . j) . k by A39, A45 ; hence y in rng (G . j) by A47, FUNCT_1:def_3; ::_thesis: verum end; ( ex_sup_of ((curry F) . j) .: (f . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17; then sup (((curry F) . j) .: (f . j)) <= sup (rng (G . j)) by A43, YELLOW_0:34; then A48: sup (((curry F) . j) .: (f . j)) <= Sup by YELLOW_2:def_5; h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6; then reconsider hj = h . j as Element of Funcs (J,FIK) by FUNCOP_1:7; A49: Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:53; sup (((curry F) . j) .: (f . j)) = sup (((curry F) . j) .: (hj . j)) by A20 .= H . (j,hj) by A2 .= ((curry H) . j) . (h . j) by Th20 .= ((Frege (curry H)) . h) . j by A34, A42, Th9 ; hence Inf <= y by A41, A48, A49, ORDERS_2:3; ::_thesis: verum end; then Inf <= inf (rng (Sups )) by YELLOW_0:33; then A50: Inf <= Inf by YELLOW_2:def_6; f in Funcs (J,(Fin K)) by A20; then Inf in X by A17, A39; then Inf <= sup X by YELLOW_2:22; hence Inf <= sup X by A50, ORDERS_2:3; ::_thesis: verum end; rng (Infs ) is_<=_than sup X proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in rng (Infs ) or x <= sup X ) assume x in rng (Infs ) ; ::_thesis: x <= sup X then consider h being set such that A51: h in dom (Frege (curry H)) and A52: x = //\ (((Frege (curry H)) . h),L) by Th13; reconsider h = h as Element of product (doms (curry H)) by A51; Inf <= sup X by A33; hence x <= sup X by A52; ::_thesis: verum end; then A53: sup (rng (Infs )) <= sup X by YELLOW_0:32; dom (curry F) = J by Th20 .= dom (curry H) by Th20 ; then Inf = Inf by A15, Th11; then Inf <= sup X by A14, A53, YELLOW_2:def_5; hence Inf = sup X by A18, ORDERS_2:2; ::_thesis: verum end; end; Lm14: for L being complete LATTICE st ( for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ) holds L is continuous proof let L be complete LATTICE; ::_thesis: ( ( for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ) implies L is continuous ) assume A1: for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ; ::_thesis: L is continuous for J, K being non empty set for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup proof let J, K be non empty set ; ::_thesis: for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds Inf = Sup let F be Function of [:J,K:], the carrier of L; ::_thesis: ( ( for j being Element of J holds rng ((curry F) . j) is directed ) implies Inf = Sup ) assume A2: for j being Element of J holds rng ((curry F) . j) is directed ; ::_thesis: Inf = Sup defpred S1[ Element of L] means ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & \$1 = Inf ) ); reconsider X = { a where a is Element of L : S1[a] } as Subset of L from DOMAIN_1:sch_7(); X is_<=_than Sup proof let a9 be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a9 in X or a9 <= Sup ) assume a9 in X ; ::_thesis: a9 <= Sup then consider a being Element of L such that A3: a9 = a and A4: ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) ; defpred S2[ set , set ] means ( \$1 in J & \$2 in K & ex b being Element of L st ( b = ((curry F) . \$1) . \$2 & a <= b ) ); consider f being V9() ManySortedSet of J such that A5: f in Funcs (J,(Fin K)) and A6: ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) by A4; consider G being DoubleIndexedSet of f,L such that A7: for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) and A8: a = Inf by A6; A9: for x being set st x in J holds ex y being set st ( y in K & S2[x,y] ) proof let x be set ; ::_thesis: ( x in J implies ex y being set st ( y in K & S2[x,y] ) ) assume x in J ; ::_thesis: ex y being set st ( y in K & S2[x,y] ) then reconsider j = x as Element of J ; Sup in rng (Sups ) by Th14; then inf (rng (Sups )) <= Sup by YELLOW_2:22; then A10: Inf <= Sup by YELLOW_2:def_6; ( not rng ((curry F) . j) is empty & rng ((curry F) . j) is directed & rng (G . j) is finite Subset of (rng ((curry F) . j)) ) by A2, A5, A7, Lm12; then consider y being Element of L such that A11: y in rng ((curry F) . j) and A12: rng (G . j) is_<=_than y by WAYBEL_0:1; consider k being set such that A13: k in dom ((curry F) . j) and A14: y = ((curry F) . j) . k by A11, FUNCT_1:def_3; reconsider k = k as Element of K by A13, Th20; take k ; ::_thesis: ( k in K & S2[x,k] ) sup (rng (G . j)) <= y by A12, YELLOW_0:32; then Sup <= y by YELLOW_2:def_5; hence ( k in K & S2[x,k] ) by A8, A14, A10, ORDERS_2:3; ::_thesis: verum end; consider g being Function such that A15: dom g = J and rng g c= K and A16: for x being set st x in J holds S2[x,g . x] from FUNCT_1:sch_5(A9); A17: dom (doms (curry F)) = dom (curry F) by FUNCT_6:59; then A18: dom g = dom (doms (curry F)) by A15, Th20; for x being set st x in dom (doms (curry F)) holds g . x in (doms (curry F)) . x proof let x be set ; ::_thesis: ( x in dom (doms (curry F)) implies g . x in (doms (curry F)) . x ) assume x in dom (doms (curry F)) ; ::_thesis: g . x in (doms (curry F)) . x then reconsider j = x as Element of J by A17; dom (curry F) = J by Th20; then (doms (curry F)) . j = dom ((curry F) . j) by FUNCT_6:22 .= K by Th20 ; hence g . x in (doms (curry F)) . x by A16; ::_thesis: verum end; then reconsider g = g as Element of product (doms (curry F)) by A18, CARD_3:9; for j being Element of J holds a <= ((Frege (curry F)) . g) . j proof let j be Element of J; ::_thesis: a <= ((Frege (curry F)) . g) . j A19: ex b being Element of L st ( b = ((curry F) . j) . (g . j) & a <= b ) by A16; ( dom (Frege (curry F)) = product (doms (curry F)) & J = dom (curry F) ) by PARTFUN1:def_2; hence a <= ((Frege (curry F)) . g) . j by A19, Th9; ::_thesis: verum end; then A20: a <= Inf by YELLOW_2:55; Inf in rng (Infs ) by Th14; then Inf <= sup (rng (Infs )) by YELLOW_2:22; then Inf <= Sup by YELLOW_2:def_5; hence a9 <= Sup by A3, A20, ORDERS_2:3; ::_thesis: verum end; then sup X <= Sup by YELLOW_0:32; then A21: Inf <= Sup by A1; Inf >= Sup by Th16; hence Inf = Sup by A21, ORDERS_2:2; ::_thesis: verum end; hence L is continuous by Lm10; ::_thesis: verum end; theorem :: WAYBEL_5:23 for L being complete LATTICE holds ( L is continuous iff for J, K being non empty set for F being Function of [:J,K:], the carrier of L for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st ( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st ( ( for j being Element of J for x being set st x in f . j holds (G . j) . x = F . (j,x) ) & a = Inf ) ) } holds Inf = sup X ) by Lm13, Lm14; begin definition let L be non empty RelStr ; attrL is completely-distributive means :Def3: :: WAYBEL_5:def 3 ( L is complete & ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup ) ); end; :: deftheorem Def3 defines completely-distributive WAYBEL_5:def_3_:_ for L being non empty RelStr holds ( L is completely-distributive iff ( L is complete & ( for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) ); registration cluster1 -element reflexive transitive antisymmetric -> 1 -element completely-distributive for RelStr ; coherence for b1 being 1 -element Poset holds b1 is completely-distributive proof let L be 1 -element Poset; ::_thesis: L is completely-distributive reconsider L9 = L as complete LATTICE ; thus L is complete ; :: according to WAYBEL_5:def_3 ::_thesis: for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup reconsider L9 = L9 as continuous LATTICE ; for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L9 holds Inf = Sup proof let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L9 holds Inf = Sup let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L9 holds Inf = Sup let F be DoubleIndexedSet of K,L9; ::_thesis: Inf = Sup for j being Element of J holds rng (F . j) is directed ; hence Inf = Sup by Lm8; ::_thesis: verum end; hence for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup ; ::_thesis: verum end; end; registration cluster non empty total reflexive transitive antisymmetric with_suprema with_infima completely-distributive for RelStr ; existence ex b1 being LATTICE st b1 is completely-distributive proof set x = the set ; set R = the Order of { the set }; RelStr(# { the set }, the Order of { the set } #) is 1 -element RelStr ; hence ex b1 being LATTICE st b1 is completely-distributive ; ::_thesis: verum end; end; theorem Th24: :: WAYBEL_5:24 for L being completely-distributive LATTICE holds L is continuous proof let L be completely-distributive LATTICE; ::_thesis: L is continuous A1: for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup by Def3; L is complete by Def3; hence L is continuous by A1, Lm9; ::_thesis: verum end; registration cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> complete continuous for RelStr ; correctness coherence for b1 being LATTICE st b1 is completely-distributive holds ( b1 is complete & b1 is continuous ); by Def3, Th24; end; theorem Th25: :: WAYBEL_5:25 for L being non empty transitive antisymmetric with_infima RelStr for x being Element of L for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds x "/\" (sup X) >= sup Y proof let L be non empty transitive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds x "/\" (sup X) >= sup Y let x be Element of L; ::_thesis: for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds x "/\" (sup X) >= sup Y let X, Y be Subset of L; ::_thesis: ( ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } implies x "/\" (sup X) >= sup Y ) assume that A1: ex_sup_of X,L and A2: ex_sup_of Y,L and A3: Y = { (x "/\" y) where y is Element of L : y in X } ; ::_thesis: x "/\" (sup X) >= sup Y Y is_<=_than x "/\" (sup X) proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in Y or y <= x "/\" (sup X) ) assume y in Y ; ::_thesis: y <= x "/\" (sup X) then consider z being Element of L such that A4: y = x "/\" z and A5: z in X by A3; A6: y <= z by A4, YELLOW_0:23; X is_<=_than sup X by A1, YELLOW_0:30; then z <= sup X by A5, LATTICE3:def_9; then A7: y <= sup X by A6, YELLOW_0:def_2; y <= x by A4, YELLOW_0:23; hence y <= x "/\" (sup X) by A7, YELLOW_0:23; ::_thesis: verum end; hence x "/\" (sup X) >= sup Y by A2, YELLOW_0:30; ::_thesis: verum end; Lm15: for L being completely-distributive LATTICE for X being non empty Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) proof let L be completely-distributive LATTICE; ::_thesis: for X being non empty Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) let X be non empty Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) let x be Element of L; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) set A = { (x "/\" y) where y is Element of L : y in X } ; set J = {1,2}; set K = (1,2) --> ({1},X); set F = (1,2) --> (({1} --> x),(id X)); A1: ((1,2) --> (({1} --> x),(id X))) . 1 = {1} --> x by FUNCT_4:63; A2: dom ((1,2) --> ({1},X)) = {1,2} by FUNCT_4:62; A3: ((1,2) --> ({1},X)) . 2 = X by FUNCT_4:63; A4: dom ((1,2) --> (({1} --> x),(id X))) = {1,2} by FUNCT_4:62; reconsider j1 = 1, j2 = 2 as Element of {1,2} by TARSKI:def_2; A5: ((1,2) --> (({1} --> x),(id X))) . 2 = id X by FUNCT_4:63; reconsider F = (1,2) --> (({1} --> x),(id X)) as ManySortedSet of {1,2} by A4, PARTFUN1:def_2, RELAT_1:def_18; A6: ((1,2) --> ({1},X)) . 1 = {1} by FUNCT_4:63; reconsider K = (1,2) --> ({1},X) as ManySortedSet of {1,2} by A2, PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in {1,2} holds not K . i is empty by A6, A3, TARSKI:def_2; then reconsider K = K as V9() ManySortedSet of {1,2} by PBOOLE:def_13; for j being set st j in {1,2} holds F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) proof let j be set ; ::_thesis: ( j in {1,2} implies F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) ) assume A7: j in {1,2} ; ::_thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) then A8: ({1,2} --> the carrier of L) . j = the carrier of L by FUNCOP_1:7; percases ( j = 1 or j = 2 ) by A7, TARSKI:def_2; suppose j = 1 ; ::_thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) hence F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) by A1, A6, A7, FUNCOP_1:7; ::_thesis: verum end; suppose j = 2 ; ::_thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) hence F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) by A5, A3, A8, FUNCT_2:7; ::_thesis: verum end; end; end; then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def_15; rng (Infs ) is_<=_than "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in rng (Infs ) or y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) ) assume y in rng (Infs ) ; ::_thesis: y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) then consider f being set such that A9: f in dom (Frege F) and A10: y = //\ (((Frege F) . f),L) by Th13; reconsider f = f as Function by A9; A11: f . j2 in K . j2 by A9, Lm6; then reconsider f2 = f . 2 as Element of X by FUNCT_4:63; A12: f . j1 in K . j1 by A9, Lm6; A13: {x,f2} c= rng ((Frege F) . f) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,f2} or z in rng ((Frege F) . f) ) assume z in {x,f2} ; ::_thesis: z in rng ((Frege F) . f) then ( z = x or z = f . 2 ) by TARSKI:def_2; then ( z = (F . j1) . (f . j1) or z = (F . j2) . (f . j2) ) by A1, A5, A6, A3, A12, A11, FUNCOP_1:7, FUNCT_1:18; hence z in rng ((Frege F) . f) by A9, Lm5; ::_thesis: verum end; x "/\" f2 in { (x "/\" y) where y is Element of L : y in X } ; then A14: x "/\" f2 <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_2:22; A15: ( ex_inf_of rng ((Frege F) . f),L & ex_inf_of {x,(f . 2)},L ) by YELLOW_0:17; y = "/\" ((rng ((Frege F) . f)),L) by A10, YELLOW_2:def_6; then y <= inf {x,f2} by A15, A13, YELLOW_0:35; then y <= x "/\" f2 by YELLOW_0:40; hence y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A14, YELLOW_0:def_2; ::_thesis: verum end; then sup (rng (Infs )) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_0:32; then A16: Sup <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_2:def_5; (x "/\") .: X = { (x "/\" y) where y is Element of L : y in X } by WAYBEL_1:61; then reconsider A9 = { (x "/\" y) where y is Element of L : y in X } as Subset of L ; ( ex_sup_of X,L & ex_sup_of A9,L ) by YELLOW_0:17; then A17: x "/\" (sup X) >= sup A9 by Th25; x "/\" (sup X) is_<=_than rng (Sups ) proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in rng (Sups ) or x "/\" (sup X) <= y ) assume y in rng (Sups ) ; ::_thesis: x "/\" (sup X) <= y then consider j being Element of {1,2} such that A18: y = Sup by Th14; percases ( j = 1 or j = 2 ) by TARSKI:def_2; suppose j = 1 ; ::_thesis: x "/\" (sup X) <= y then rng (F . j) = {x} by A1, FUNCOP_1:8; then Sup = sup {x} by YELLOW_2:def_5; then y = x by A18, YELLOW_0:39; hence x "/\" (sup X) <= y by YELLOW_0:23; ::_thesis: verum end; suppose j = 2 ; ::_thesis: x "/\" (sup X) <= y then rng (F . j) = X by A5, RELAT_1:45; then y = sup X by A18, YELLOW_2:def_5; hence x "/\" (sup X) <= y by YELLOW_0:23; ::_thesis: verum end; end; end; then x "/\" (sup X) <= inf (rng (Sups )) by YELLOW_0:33; then x "/\" (sup X) <= Inf by YELLOW_2:def_6; then x "/\" (sup X) <= Sup by Def3; then x "/\" (sup X) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A16, YELLOW_0:def_2; hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A17, YELLOW_0:def_3; ::_thesis: verum end; theorem Th26: :: WAYBEL_5:26 for L being completely-distributive LATTICE for X being Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) proof let L be completely-distributive LATTICE; ::_thesis: for X being Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) let X be Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) let x be Element of L; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) set A = { (x "/\" y) where y is Element of L : y in X } ; percases ( X is empty or not X is empty ) ; supposeA1: X is empty ; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) now__::_thesis:_not__{__(x_"/\"_y)_where_y_is_Element_of_L_:_y_in_X__}__<>_{} set z = the Element of { (x "/\" y) where y is Element of L : y in X } ; assume { (x "/\" y) where y is Element of L : y in X } <> {} ; ::_thesis: contradiction then the Element of { (x "/\" y) where y is Element of L : y in X } in { (x "/\" y) where y is Element of L : y in X } ; then ex y being Element of L st ( the Element of { (x "/\" y) where y is Element of L : y in X } = x "/\" y & y in X ) ; hence contradiction by A1; ::_thesis: verum end; then A2: "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) = Bottom L by YELLOW_0:def_11; sup X = Bottom L by A1, YELLOW_0:def_11; hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A2, WAYBEL_1:3; ::_thesis: verum end; suppose not X is empty ; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by Lm15; ::_thesis: verum end; end; end; registration cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> Heyting for RelStr ; correctness coherence for b1 being LATTICE st b1 is completely-distributive holds b1 is Heyting ; proof let L be LATTICE; ::_thesis: ( L is completely-distributive implies L is Heyting ) assume L is completely-distributive ; ::_thesis: L is Heyting then reconsider L = L as completely-distributive LATTICE ; for X being Subset of L for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by Th26; then for x being Element of L holds x "/\" is lower_adjoint by WAYBEL_1:64; hence L is Heyting by WAYBEL_1:def_19; ::_thesis: verum end; end; begin definition let L be non empty RelStr ; mode CLSubFrame of L is non empty full infs-inheriting directed-sups-inheriting SubRelStr of L; end; theorem Th27: :: WAYBEL_5:27 for L being complete LATTICE for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds rng (Infs ) is directed proof let L be complete LATTICE; ::_thesis: for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds rng (Infs ) is directed let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds rng (Infs ) is directed let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds rng (Infs ) is directed let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies rng (Infs ) is directed ) set X = rng (Infs ); assume A1: for j being Element of J holds rng (F . j) is directed ; ::_thesis: rng (Infs ) is directed for x, y being Element of L st x in rng (Infs ) & y in rng (Infs ) holds ex z being Element of L st ( z in rng (Infs ) & x <= z & y <= z ) proof let x, y be Element of L; ::_thesis: ( x in rng (Infs ) & y in rng (Infs ) implies ex z being Element of L st ( z in rng (Infs ) & x <= z & y <= z ) ) assume that A2: x in rng (Infs ) and A3: y in rng (Infs ) ; ::_thesis: ex z being Element of L st ( z in rng (Infs ) & x <= z & y <= z ) consider h being set such that A4: h in dom (Frege F) and A5: y = //\ (((Frege F) . h),L) by A3, Th13; reconsider h = h as Function by A4; reconsider H = (Frege F) . h as Function of J, the carrier of L by A4, Th10; consider g being set such that A6: g in dom (Frege F) and A7: x = //\ (((Frege F) . g),L) by A2, Th13; reconsider g = g as Function by A6; reconsider G = (Frege F) . g as Function of J, the carrier of L by A6, Th10; A8: ex_inf_of rng ((Frege F) . g),L by YELLOW_0:17; defpred S1[ set , set ] means ( \$1 in J & \$2 in K . \$1 & ( for c being Element of L st c = (F . \$1) . \$2 holds ( ( for a being Element of L st a = G . \$1 holds a <= c ) & ( for b being Element of L st b = H . \$1 holds b <= c ) ) ) ); A9: for j being Element of J ex k being Element of K . j st ( G . j <= (F . j) . k & H . j <= (F . j) . k ) proof let j be Element of J; ::_thesis: ex k being Element of K . j st ( G . j <= (F . j) . k & H . j <= (F . j) . k ) j in J ; then A10: j in dom F by PARTFUN1:def_2; then A11: g . j in dom (F . j) by A6, Th9; j in J ; then A12: j in dom F by PARTFUN1:def_2; then G . j = (F . j) . (g . j) by A6, Th9; then A13: G . j in rng (F . j) by A11, FUNCT_1:def_3; A14: h . j in dom (F . j) by A4, A10, Th9; H . j = (F . j) . (h . j) by A4, A12, Th9; then A15: H . j in rng (F . j) by A14, FUNCT_1:def_3; rng (F . j) is directed Subset of L by A1; then consider c being Element of L such that A16: c in rng (F . j) and A17: ( G . j <= c & H . j <= c ) by A13, A15, WAYBEL_0:def_1; consider k being set such that A18: k in dom (F . j) and A19: c = (F . j) . k by A16, FUNCT_1:def_3; reconsider k = k as Element of K . j by A18; take k ; ::_thesis: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) thus ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A17, A19; ::_thesis: verum end; A20: for j being set st j in J holds ex k being set st ( k in union (rng K) & S1[j,k] ) proof let j9 be set ; ::_thesis: ( j9 in J implies ex k being set st ( k in union (rng K) & S1[j9,k] ) ) assume j9 in J ; ::_thesis: ex k being set st ( k in union (rng K) & S1[j9,k] ) then reconsider j = j9 as Element of J ; consider k being Element of K . j such that A21: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A9; take k ; ::_thesis: ( k in union (rng K) & S1[j9,k] ) j in J ; then j in dom K by PARTFUN1:def_2; then K . j in rng K by FUNCT_1:def_3; hence k in union (rng K) by TARSKI:def_4; ::_thesis: S1[j9,k] thus S1[j9,k] by A21; ::_thesis: verum end; consider f being Function such that A22: dom f = J and rng f c= union (rng K) and A23: for j being set st j in J holds S1[j,f . j] from FUNCT_1:sch_5(A20); A24: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_F)_holds_ f_._x_in_(doms_F)_._x let x be set ; ::_thesis: ( x in dom (doms F) implies f . x in (doms F) . x ) assume x in dom (doms F) ; ::_thesis: f . x in (doms F) . x then A25: x in dom F by FUNCT_6:59; then reconsider j = x as Element of J ; (doms F) . x = dom (F . j) by A25, FUNCT_6:22 .= K . j by FUNCT_2:def_1 ; hence f . x in (doms F) . x by A23; ::_thesis: verum end; dom f = dom F by A22, PARTFUN1:def_2 .= dom (doms F) by FUNCT_6:59 ; then f in product (doms F) by A24, CARD_3:9; then A26: f in dom (Frege F) by PARTFUN1:def_2; then reconsider Ff = (Frege F) . f as Function of J, the carrier of L by Th10; take z = Inf ; ::_thesis: ( z in rng (Infs ) & x <= z & y <= z ) thus z in rng (Infs ) by A26, Th13; ::_thesis: ( x <= z & y <= z ) A27: x = "/\" ((rng ((Frege F) . g)),L) by A7, YELLOW_2:def_6; now__::_thesis:_for_j_being_Element_of_J_holds_x_<=_Ff_._j let j be Element of J; ::_thesis: x <= Ff . j A28: j in J ; then j in dom G by FUNCT_2:def_1; then A29: G . j in rng G by FUNCT_1:def_3; j in dom F by A28, PARTFUN1:def_2; then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9; then A30: G . j <= Ff . j by A23; x is_<=_than rng G by A27, A8, YELLOW_0:def_10; then x <= G . j by A29, LATTICE3:def_8; hence x <= Ff . j by A30, ORDERS_2:3; ::_thesis: verum end; hence x <= z by YELLOW_2:55; ::_thesis: y <= z A31: ex_inf_of rng ((Frege F) . h),L by YELLOW_0:17; A32: y = "/\" ((rng ((Frege F) . h)),L) by A5, YELLOW_2:def_6; now__::_thesis:_for_j_being_Element_of_J_holds_y_<=_Ff_._j let j be Element of J; ::_thesis: y <= Ff . j A33: j in J ; then j in dom H by FUNCT_2:def_1; then A34: H . j in rng H by FUNCT_1:def_3; j in dom F by A33, PARTFUN1:def_2; then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9; then A35: H . j <= Ff . j by A23; y is_<=_than rng H by A32, A31, YELLOW_0:def_10; then y <= H . j by A34, LATTICE3:def_8; hence y <= Ff . j by A35, ORDERS_2:3; ::_thesis: verum end; hence y <= z by YELLOW_2:55; ::_thesis: verum end; hence rng (Infs ) is directed by WAYBEL_0:def_1; ::_thesis: verum end; theorem :: WAYBEL_5:28 for L being complete LATTICE st L is continuous holds for S being CLSubFrame of L holds S is continuous LATTICE proof let L be complete LATTICE; ::_thesis: ( L is continuous implies for S being CLSubFrame of L holds S is continuous LATTICE ) assume A1: L is continuous ; ::_thesis: for S being CLSubFrame of L holds S is continuous LATTICE let S be CLSubFrame of L; ::_thesis: S is continuous LATTICE reconsider L9 = L as complete LATTICE ; A2: S is complete LATTICE by YELLOW_2:30; for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup proof let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let F be DoubleIndexedSet of K,S; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup ) assume A3: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup now__::_thesis:_for_j_being_set_st_j_in_J_holds_ F_._j_is_Function_of_(K_._j),((J_-->_the_carrier_of_L)_._j) let j be set ; ::_thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) ) assume A4: j in J ; ::_thesis: F . j is Function of (K . j),((J --> the carrier of L) . j) then reconsider j9 = j as Element of J ; A5: ( F . j9 is Function of (K . j9), the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def_13; (J --> the carrier of L) . j = the carrier of L by A4, FUNCOP_1:7; hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A5, FUNCT_2:7; ::_thesis: verum end; then reconsider F9 = F as DoubleIndexedSet of K,L by PBOOLE:def_15; ex_inf_of rng (Sups ),L by YELLOW_0:17; then A6: "/\" ((rng (Sups )),L) in the carrier of S by YELLOW_0:def_18; now__::_thesis:_for_x_being_set_st_x_in_rng_(Sups_)_holds_ x_in_rng_(Sups_) let x be set ; ::_thesis: ( x in rng (Sups ) implies x in rng (Sups ) ) assume x in rng (Sups ) ; ::_thesis: x in rng (Sups ) then consider j being Element of J such that A7: x = Sup by Th14; A8: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17; x = sup (rng (F9 . j)) by A7, YELLOW_2:def_5 .= sup (rng (F . j)) by A8, WAYBEL_0:7 .= Sup by YELLOW_2:def_5 ; hence x in rng (Sups ) by Th14; ::_thesis: verum end; then A9: rng (Sups ) c= rng (Sups ) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_rng_(Sups_)_holds_ x_in_rng_(Sups_) let x be set ; ::_thesis: ( x in rng (Sups ) implies x in rng (Sups ) ) assume x in rng (Sups ) ; ::_thesis: x in rng (Sups ) then consider j being Element of J such that A10: x = Sup by Th14; A11: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17; x = sup (rng (F . j)) by A10, YELLOW_2:def_5 .= sup (rng (F9 . j)) by A11, WAYBEL_0:7 .= Sup by YELLOW_2:def_5 ; hence x in rng (Sups ) by Th14; ::_thesis: verum end; then rng (Sups ) c= rng (Sups ) by TARSKI:def_3; then ( ex_inf_of rng (Sups ),L9 & rng (Sups ) = rng (Sups ) ) by A9, XBOOLE_0:def_10, YELLOW_0:17; then inf (rng (Sups )) = inf (rng (Sups )) by A6, YELLOW_0:63; then A12: Inf = inf (rng (Sups )) by YELLOW_2:def_6; now__::_thesis:_for_x_being_set_st_x_in_rng_(Infs_)_holds_ x_in_rng_(Infs_) let x be set ; ::_thesis: ( x in rng (Infs ) implies x in rng (Infs ) ) assume x in rng (Infs ) ; ::_thesis: x in rng (Infs ) then consider f being set such that A13: f in dom (Frege F) and A14: x = //\ (((Frege F) . f),S) by Th13; reconsider f = f as Function by A13; (Frege F) . f is Function of J, the carrier of S by A13, Th10; then A15: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def_19; A16: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17; then A17: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A15, YELLOW_0:def_18; x = "/\" ((rng ((Frege F) . f)),S) by A14, YELLOW_2:def_6 .= "/\" ((rng ((Frege F9) . f)),L) by A15, A16, A17, YELLOW_0:63 .= //\ (((Frege F9) . f),L) by YELLOW_2:def_6 ; hence x in rng (Infs ) by A13, Th13; ::_thesis: verum end; then A18: rng (Infs ) c= rng (Infs ) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_rng_(/\\_((Frege_F9),L))_holds_ x_in_rng_(Infs_) let x be set ; ::_thesis: ( x in rng (/\\ ((Frege F9),L)) implies x in rng (Infs ) ) assume x in rng (/\\ ((Frege F9),L)) ; ::_thesis: x in rng (Infs ) then consider f being set such that A19: f in dom (Frege F9) and A20: x = //\ (((Frege F9) . f),L) by Th13; reconsider f = f as Element of product (doms F9) by A19; (Frege F) . f is Function of J, the carrier of S by A19, Th10; then A21: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def_19; A22: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17; then A23: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A21, YELLOW_0:def_18; x = "/\" ((rng ((Frege F9) . f)),L) by A20, YELLOW_2:def_6 .= "/\" ((rng ((Frege F) . f)),S) by A21, A22, A23, YELLOW_0:63 .= //\ (((Frege F) . f),S) by YELLOW_2:def_6 ; hence x in rng (Infs ) by A19, Th13; ::_thesis: verum end; then rng (/\\ ((Frege F9),L)) c= rng (/\\ ((Frege F),S)) by TARSKI:def_3; then A24: rng (Infs ) = rng (Infs ) by A18, XBOOLE_0:def_10; for j being Element of J holds rng (F9 . j) is directed proof let j be Element of J; ::_thesis: rng (F9 . j) is directed rng (F . j) is directed by A3; hence rng (F9 . j) is directed by YELLOW_2:7; ::_thesis: verum end; then A25: Inf = Sup by A1, Lm8; ( ex_sup_of rng (/\\ ((Frege F9),L)),L9 & rng (Infs ) is non empty directed Subset of S ) by A2, A3, Th27, YELLOW_0:17; then sup (rng (Infs )) = sup (rng (Infs )) by A24, WAYBEL_0:7; then Sup = sup (rng (Infs )) by YELLOW_2:def_5 .= Sup by YELLOW_2:def_5 ; hence Inf = Sup by A25, A12, YELLOW_2:def_6; ::_thesis: verum end; hence S is continuous LATTICE by A2, Lm9; ::_thesis: verum end; theorem Th29: :: WAYBEL_5:29 for L being complete LATTICE for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is onto ) holds S is complete LATTICE proof let L be complete LATTICE; ::_thesis: for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is onto ) holds S is complete LATTICE let S be non empty Poset; ::_thesis: ( ex g being Function of L,S st ( g is infs-preserving & g is onto ) implies S is complete LATTICE ) given g being Function of L,S such that A1: g is infs-preserving and A2: g is onto ; ::_thesis: S is complete LATTICE for A being Subset of S holds ex_inf_of A,S proof let A be Subset of S; ::_thesis: ex_inf_of A,S set Y = g " A; rng g = the carrier of S by A2, FUNCT_2:def_3; then A3: A = g .: (g " A) by FUNCT_1:77; ( ex_inf_of g " A,L & g preserves_inf_of g " A ) by A1, WAYBEL_0:def_32, YELLOW_0:17; hence ex_inf_of A,S by A3, WAYBEL_0:def_30; ::_thesis: verum end; then S is non empty complete Poset by YELLOW_2:28; hence S is complete LATTICE ; ::_thesis: verum end; notation let J, y be set ; synonym J => y for J --> y; end; registration let J, y be set ; clusterJ => y -> J -defined total for J -defined Function; coherence for b1 being J -defined Function st b1 = J => y holds b1 is total ; end; definition let A, B, J be set ; let f be Function of A,B; :: original: => redefine funcJ => f -> ManySortedFunction of J --> A,J --> B; coherence J => f is ManySortedFunction of J --> A,J --> B proof set JA = J --> A; set JB = J --> B; for j being set st j in J holds (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) proof let j be set ; ::_thesis: ( j in J implies (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) ) assume A1: j in J ; ::_thesis: (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) then ( (J --> A) . j = A & (J --> B) . j = B ) by FUNCOP_1:7; hence (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) by A1, FUNCOP_1:7; ::_thesis: verum end; hence J => f is ManySortedFunction of J --> A,J --> B by PBOOLE:def_15; ::_thesis: verum end; end; theorem Th30: :: WAYBEL_5:30 for J being non empty set for A, B being set for f being Function of A,B for g being Function of B,A st g * f = id A holds (J => g) ** (J => f) = id (J --> A) proof let J be non empty set ; ::_thesis: for A, B being set for f being Function of A,B for g being Function of B,A st g * f = id A holds (J => g) ** (J => f) = id (J --> A) let A, B be set ; ::_thesis: for f being Function of A,B for g being Function of B,A st g * f = id A holds (J => g) ** (J => f) = id (J --> A) let f be Function of A,B; ::_thesis: for g being Function of B,A st g * f = id A holds (J => g) ** (J => f) = id (J --> A) let g be Function of B,A; ::_thesis: ( g * f = id A implies (J => g) ** (J => f) = id (J --> A) ) set F = (J => g) ** (J => f); dom ((J => g) ** (J => f)) = J by MSUALG_3:2; then reconsider F = (J => g) ** (J => f) as ManySortedSet of J by PARTFUN1:def_2, RELAT_1:def_18; assume A1: g * f = id A ; ::_thesis: (J => g) ** (J => f) = id (J --> A) A2: for j being set st j in J holds F . j = id ((J --> A) . j) proof let j be set ; ::_thesis: ( j in J implies F . j = id ((J --> A) . j) ) assume A3: j in J ; ::_thesis: F . j = id ((J --> A) . j) then A4: (J --> A) . j = A by FUNCOP_1:7; ( (J => g) . j = g & (J => f) . j = f ) by A3, FUNCOP_1:7; hence F . j = id ((J --> A) . j) by A1, A3, A4, MSUALG_3:2; ::_thesis: verum end; now__::_thesis:_for_j_being_set_st_j_in_J_holds_ F_._j_is_Function_of_((J_-->_A)_._j),((J_-->_A)_._j) let j be set ; ::_thesis: ( j in J implies F . j is Function of ((J --> A) . j),((J --> A) . j) ) assume j in J ; ::_thesis: F . j is Function of ((J --> A) . j),((J --> A) . j) then F . j = id ((J --> A) . j) by A2; hence F . j is Function of ((J --> A) . j),((J --> A) . j) ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of J --> A,J --> A by PBOOLE:def_15; for j being set st j in J holds F . j = id ((J --> A) . j) by A2; hence (J => g) ** (J => f) = id (J --> A) by MSUALG_3:def_1; ::_thesis: verum end; theorem Th31: :: WAYBEL_5:31 for J, A being non empty set for B being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B proof let J, A be non empty set ; ::_thesis: for B being set for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B let B be set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,A for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B let F be DoubleIndexedSet of K,A; ::_thesis: for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B let f be Function of A,B; ::_thesis: (J => f) ** F is DoubleIndexedSet of K,B set fF = (J => f) ** F; dom ((J => f) ** F) = J by MSUALG_3:2; then reconsider fF = (J => f) ** F as ManySortedSet of J by PARTFUN1:def_2, RELAT_1:def_18; for j being set st j in J holds fF . j is Function of (K . j),((J --> B) . j) proof let j be set ; ::_thesis: ( j in J implies fF . j is Function of (K . j),((J --> B) . j) ) assume A1: j in J ; ::_thesis: fF . j is Function of (K . j),((J --> B) . j) then reconsider j9 = j as Element of J ; reconsider Fj = F . j9 as Function of (K . j),A ; A2: fF . j = ((J => f) . j) * (F . j) by A1, MSUALG_3:2 .= f * Fj by FUNCOP_1:7 ; (J --> B) . j = B by A1, FUNCOP_1:7; hence fF . j is Function of (K . j),((J --> B) . j) by A2; ::_thesis: verum end; hence (J --> f) ** F is DoubleIndexedSet of K,B by PBOOLE:def_15; ::_thesis: verum end; theorem Th32: :: WAYBEL_5:32 for J, A, B being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds doms ((J => f) ** F) = doms F proof let J, A, B be non empty set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,A for f being Function of A,B holds doms ((J => f) ** F) = doms F let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,A for f being Function of A,B holds doms ((J => f) ** F) = doms F let F be DoubleIndexedSet of K,A; ::_thesis: for f being Function of A,B holds doms ((J => f) ** F) = doms F let f be Function of A,B; ::_thesis: doms ((J => f) ** F) = doms F A1: dom (doms ((J => f) ** F)) = dom ((J => f) ** F) by FUNCT_6:59 .= J by MSUALG_3:2 ; A2: now__::_thesis:_for_x_being_set_st_x_in_J_holds_ (doms_((J_=>_f)_**_F))_._x_=_(doms_F)_._x let x be set ; ::_thesis: ( x in J implies (doms ((J => f) ** F)) . x = (doms F) . x ) assume A3: x in J ; ::_thesis: (doms ((J => f) ** F)) . x = (doms F) . x then reconsider j = x as Element of J ; A4: j in dom F by A3, PARTFUN1:def_2; A5: ( rng (F . j) c= A & dom f = A ) by FUNCT_2:def_1; j in dom ((J => f) ** F) by A1, A3, FUNCT_6:59; then (doms ((J => f) ** F)) . j = dom (((J => f) ** F) . j) by FUNCT_6:22 .= dom (((J => f) . j) * (F . j)) by MSUALG_3:2 .= dom (f * (F . j)) by FUNCOP_1:7 .= dom (F . j) by A5, RELAT_1:27 .= (doms F) . j by A4, FUNCT_6:22 ; hence (doms ((J => f) ** F)) . x = (doms F) . x ; ::_thesis: verum end; dom (doms F) = dom F by FUNCT_6:59 .= J by PARTFUN1:def_2 ; hence doms ((J => f) ** F) = doms F by A1, A2, FUNCT_1:2; ::_thesis: verum end; theorem :: WAYBEL_5:33 for L being complete LATTICE st L is continuous holds for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds S is continuous LATTICE proof let L be complete LATTICE; ::_thesis: ( L is continuous implies for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds S is continuous LATTICE ) assume A1: L is continuous ; ::_thesis: for S being non empty Poset st ex g being Function of L,S st ( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds S is continuous LATTICE let S be non empty Poset; ::_thesis: ( ex g being Function of L,S st ( g is infs-preserving & g is directed-sups-preserving & g is onto ) implies S is continuous LATTICE ) given g being Function of L,S such that A2: ( g is infs-preserving & g is directed-sups-preserving ) and A3: g is onto ; ::_thesis: S is continuous LATTICE reconsider S9 = S as complete LATTICE by A2, A3, Th29; for J being non empty set for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup proof let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds Inf = Sup let F be DoubleIndexedSet of K,S9; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup ) assume A4: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup consider d being Function of S,L such that A5: [g,d] is Galois and for t being Element of S holds d . t is_minimum_of g " (uparrow t) by A2, WAYBEL_1:14; reconsider dF = (J => d) ** F as DoubleIndexedSet of K,L by Th31; A6: ( ex_inf_of rng (Sups ),L & g preserves_inf_of rng (Sups ) ) by A2, WAYBEL_0:def_32, YELLOW_0:17; for t being Element of S holds d . t is_minimum_of g " {t} by A3, A5, WAYBEL_1:22; then A7: g * d = id S by WAYBEL_1:23; A8: for f being set st f in dom (Frege dF) holds rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) proof let f be set ; ::_thesis: ( f in dom (Frege dF) implies rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) ) assume A9: f in dom (Frege dF) ; ::_thesis: rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) then reconsider f = f as Element of product (doms dF) ; A10: dom (Frege dF) = product (doms dF) by PARTFUN1:def_2 .= product (doms F) by Th32 .= dom (Frege F) by PARTFUN1:def_2 ; A11: dom ((Frege dF) . f) = dom dF by A9, Th8 .= J by PARTFUN1:def_2 ; A12: now__::_thesis:_for_i_being_set_st_i_in_J_holds_ (g_*_((Frege_dF)_._f))_._i_=_((Frege_F)_._f)_._i let i be set ; ::_thesis: ( i in J implies (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i ) assume A13: i in J ; ::_thesis: (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i then reconsider j = i as Element of J ; A14: j in dom F by A13, PARTFUN1:def_2; A15: j in dom dF by A13, PARTFUN1:def_2; then f . j in dom (dF . j) by A9, Th9; then f . j in dom (((J => d) . j) * (F . j)) by MSUALG_3:2; then A16: f . j in dom (d * (F . j)) by FUNCOP_1:7; (g * ((Frege dF) . f)) . j = g . (((Frege dF) . f) . j) by A11, FUNCT_1:13 .= g . ((dF . j) . (f . j)) by A9, A15, Th9 .= g . ((((J => d) . j) * (F . j)) . (f . j)) by MSUALG_3:2 .= g . ((d * (F . j)) . (f . j)) by FUNCOP_1:7 .= (g * (d * (F . j))) . (f . j) by A16, FUNCT_1:13 .= ((id the carrier of S) * (F . j)) . (f . j) by A7, RELAT_1:36 .= (F . j) . (f . j) by FUNCT_2:17 .= ((Frege F) . f) . j by A9, A10, A14, Th9 ; hence (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i ; ::_thesis: verum end; dom g = the carrier of L by FUNCT_2:def_1; then rng ((Frege dF) . f) c= dom g ; then A17: dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f) by RELAT_1:27; dom ((Frege F) . f) = dom F by A9, A10, Th8 .= J by PARTFUN1:def_2 ; then rng ((Frege F) . f) = rng (g * ((Frege dF) . f)) by A11, A17, A12, FUNCT_1:2 .= g .: (rng ((Frege dF) . f)) by RELAT_1:127 ; hence rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) ; ::_thesis: verum end; A18: rng (Infs ) c= g .: (rng (Infs )) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Infs ) or y in g .: (rng (Infs )) ) assume y in rng (Infs ) ; ::_thesis: y in g .: (rng (Infs )) then consider f being set such that A19: f in dom (Frege F) and A20: y = //\ (((Frege F) . f),S) by Th13; reconsider f = f as Element of product (doms F) by A19; reconsider f9 = f as Element of product (doms dF) by Th32; set X = rng ((Frege dF) . f9); A21: ( g preserves_inf_of rng ((Frege dF) . f9) & ex_inf_of rng ((Frege dF) . f9),L ) by A2, WAYBEL_0:def_32, YELLOW_0:17; A22: dom (Frege dF) = product (doms dF) by PARTFUN1:def_2 .= product (doms F) by Th32 .= dom (Frege F) by PARTFUN1:def_2 ; then rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A19; then y = "/\" ((g .: (rng ((Frege dF) . f))),S) by A20, YELLOW_2:def_6; then A23: y = g . (inf (rng ((Frege dF) . f9))) by A21, WAYBEL_0:def_30 .= g . (Inf ) by YELLOW_2:def_6 ; Inf in rng (Infs ) by A19, A22, Th13; hence y in g .: (rng (Infs )) by A23, FUNCT_2:35; ::_thesis: verum end; A24: g .: (rng (Infs )) c= rng (Infs ) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g .: (rng (Infs )) or y in rng (Infs ) ) assume y in g .: (rng (Infs )) ; ::_thesis: y in rng (Infs ) then consider x being set such that x in the carrier of L and A25: x in rng (Infs ) and A26: y = g . x by FUNCT_2:64; consider f being set such that A27: f in dom (Frege dF) and A28: x = //\ (((Frege dF) . f),L) by A25, Th13; reconsider f = f as Element of product (doms dF) by A27; set X = rng ((Frege dF) . f); ( g preserves_inf_of rng ((Frege dF) . f) & ex_inf_of rng ((Frege dF) . f),L ) by A2, WAYBEL_0:def_32, YELLOW_0:17; then inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f))) by WAYBEL_0:def_30; then A29: y = inf (g .: (rng ((Frege dF) . f))) by A26, A28, YELLOW_2:def_6; A30: dom (Frege dF) = product (doms dF) by PARTFUN1:def_2 .= product (doms F) by Th32 .= dom (Frege F) by PARTFUN1:def_2 ; reconsider f9 = f as Element of product (doms F) by Th32; rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A27; then y = Inf by A29, YELLOW_2:def_6; hence y in rng (Infs ) by A27, A30, Th13; ::_thesis: verum end; A31: d is monotone by A5, WAYBEL_1:8; A32: for j being Element of J holds rng (dF . j) is directed proof let j be Element of J; ::_thesis: rng (dF . j) is directed (J => d) . j = d by FUNCOP_1:7; then A33: rng (dF . j) = rng (d * (F . j)) by MSUALG_3:2 .= d .: (rng (F . j)) by RELAT_1:127 ; rng (F . j) is directed by A4; hence rng (dF . j) is directed by A31, A33, YELLOW_2:15; ::_thesis: verum end; then ( rng (Infs ) is directed & not rng (Infs ) is empty ) by Th27; then A34: g preserves_sup_of rng (Infs ) by A2, WAYBEL_0:def_37; reconsider gdF = (J => g) ** dF as DoubleIndexedSet of K,S ; A35: ex_sup_of rng (Infs ),L by YELLOW_0:17; A36: rng (Sups ) c= g .: (rng (Sups )) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Sups ) or y in g .: (rng (Sups )) ) assume y in rng (Sups ) ; ::_thesis: y in g .: (rng (Sups )) then consider j being Element of J such that A37: y = Sup by Th14; gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2 .= g * (dF . j) by FUNCOP_1:7 ; then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127; then A38: y = sup (g .: (rng (dF . j))) by A37, YELLOW_2:def_5; rng (dF . j) is directed by A32; then A39: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def_37; ex_sup_of rng (dF . j),L by YELLOW_0:17; then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A39, WAYBEL_0:def_31; then A40: y = g . (Sup ) by A38, YELLOW_2:def_5; Sup in rng (Sups ) by Th14; hence y in g .: (rng (Sups )) by A40, FUNCT_2:35; ::_thesis: verum end; A41: g .: (rng (Sups )) c= rng (Sups ) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g .: (rng (Sups )) or y in rng (Sups ) ) assume y in g .: (rng (Sups )) ; ::_thesis: y in rng (Sups ) then consider x being set such that x in the carrier of L and A42: x in rng (Sups ) and A43: y = g . x by FUNCT_2:64; consider j being Element of J such that A44: x = Sup by A42, Th14; rng (dF . j) is directed by A32; then A45: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def_37; ex_sup_of rng (dF . j),L by YELLOW_0:17; then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A45, WAYBEL_0:def_31; then A46: y = sup (g .: (rng (dF . j))) by A43, A44, YELLOW_2:def_5; gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2 .= g * (dF . j) by FUNCOP_1:7 ; then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127; then y = Sup by A46, YELLOW_2:def_5; hence y in rng (Sups ) by Th14; ::_thesis: verum end; F = (id (J --> the carrier of S)) ** F by MSUALG_3:4 .= ((J --> g) ** (J --> d)) ** F by A7, Th30 .= gdF by PBOOLE:140 ; then Inf = inf (rng (Sups )) by YELLOW_2:def_6 .= inf (g .: (rng (Sups ))) by A36, A41, XBOOLE_0:def_10 .= g . (inf (rng (Sups ))) by A6, WAYBEL_0:def_30 .= g . (Inf ) by YELLOW_2:def_6 .= g . (Sup ) by A1, A32, Lm8 .= g . (sup (rng (Infs ))) by YELLOW_2:def_5 .= sup (g .: (rng (Infs ))) by A34, A35, WAYBEL_0:def_31 .= sup (rng (Infs )) by A24, A18, XBOOLE_0:def_10 .= Sup by YELLOW_2:def_5 ; hence Inf = Sup ; ::_thesis: verum end; hence S is continuous LATTICE by Lm9; ::_thesis: verum end;