proposition: Lemma setX_lattice_finite_sup g (r := order_product g) E (z := supremum r E): order_fam g -> (forall i, inc i (domain g) -> lattice (Vg g i)) -> finite_set E -> sub E (substrate r) -> nonempty E -> (inc z (substrate r) /\ forall i, inc i (domain g) -> Vg z i = supremum (Vg g i)(fun_image E (Vg^~i))).
proof: Proof. move => ofg alg fsE sEs neE. move: (setX_lattice ofg alg) => lp. move: (lattice_finite_sup2 lp fsE neE sEs) => hs. move: (supremum_pr (proj1 lp) sEs hs) => []; rewrite -/r -/z => pa pb. move: pa => [pa1 pa2]; split; first by exact. move => i idg. have pc: sub E (productb (fam_of_substrates g)). by move: sEs; rewrite (proj2 (order_product_osr _)) /prod_of_substrates. move: (sup_in_product ofg pc) => [ha hb]. move: hs; rewrite - ha => hc; rewrite /z /r (hb hc); aw; rewrite LgV//. have fgf: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops. have idf: inc i (domain (fam_of_substrates g)) by rewrite /fam_of_substrates;aw. have fp: function (pr_i (fam_of_substrates g) i) by fprops. have sE: sub E (source (pr_i (fam_of_substrates g) i)) by rewrite /pr_i; aw. congr (supremum (Vg g i) _); set_extens t. move => /(Vf_image_P fp sE) [y ye ->]; apply /funI_P;ex_tac. by rewrite pri_V //; apply:pc. move /funI_P => [y ye ->]; apply /(Vf_image_P fp sE). ex_tac;by rewrite pri_V //; apply:pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)