proposition: Lemma ex4e (S := (ex4_system (proj1 ex4d_orderIr_prop3))) (S' := (prl_exa2_system \1c (ps_preorder_r S) (ps_substrate_r S))) (u:= (Lg (psI S) (fun z => (Lf (fun i => \0c) (Vg (psE S) z) \1c)))): [/\ prl_same_index S S', prl_map2_compat S S' u, (forall i, inc i (psI S) -> surjection (Vg u i)) & ~(surjection (projective_limit_fun S S' u))].
proof: Proof. move: (ex4_system_prop (proj1 ex4d_orderIr_prop3)). rewrite -/S; move => [E_S I_S r_S f_S]. move:(prl_exa2_prop \1c (ps_preorder_r S) (ps_substrate_r S)). rewrite -/S'; move => [E_S' I_S' r_S' f_S']. have pa: projective_limit S' = diagonal_graphp \1c (psI S). apply:prl_exa2_prop2; rewrite r_S. move:(proj1 ex4d_orderIr_prop3)=>[];set r:= ex4d_orderr (\Po Nat). move => _ _ sr rdr _ x y xsr ysr; move/right_directedP: rdr => [or h]. rewrite - (ps_substrate_r S) r_S in xsr ysr. move: (h _ _ xsr ysr)=> [z [za zb]]; exists z; split => //. by move: (arg2_sr za); rewrite -(ps_substrate_r S) r_S. have [y ye]: nonempty (projective_limit S'). rewrite pa; exists (cst_graph (psI S) \0c); apply/diagonal_graph_P. split; rewrite/constantgp; aw; trivial. by split; aww => i j iI jI;rewrite !LgV//. have ha: fgraph (cst_graph (psI S) \0c) by fprops. move => t /(range_gP ha); aw. trivial; move => [x xi ->]; rewrite LgV//; apply:set1_1. have pc: prl_same_index S S' by []. have pd: prl_map2_compat S S' u. rewrite /u; set W := (fun _ : Set => \0c). have ES' i: inc i (psI S)-> \1c = Vg (psE S') i by move=> iI;rewrite E_S' LgV. have hu i: inc i (psI S) -> lf_axiom W (Vg (psE S) i) \1c. move => iI t tE; apply:set1_1. have hv i: inc i (psI S) -> function_prop (Lf W (Vg (psE S) i) \1c) (Vg (psE S) i) (Vg (psE S') i). by move => iI; saw;[ apply:(lf_function (hu _ iI)) | apply: ES']. split; aww; first by move => i iI; rewrite LgV//; apply: hv. move => i j lij. move:(arg1_sr lij) (arg2_sr lij); rewrite ps_substrate_r => iI jI. move: (ps_function_f lij); aw;move => [fij sij tij]. move: (hv _ iI) (hv _ jI)=> [fi si ti][fj sj tj]. have ha: Lf W (Vg (psE S) i) \1c \coP Vg (psf S) (J i j) by split => //; aw. have hb: Vg (psf S') (J i j) \coP Lf W (Vg (psE S) j) \1c. by rewrite f_S' LgV //;split; fprops; aw. rewrite LgV //LgV//; apply: function_exten; aw; trivial. - by apply: compf_f. - by apply: compf_f. - by rewrite f_S' LgV//; aw. - rewrite sij => t te. have ts: inc t (source (Vg (psf S) (J i j))) by ue. have tss:inc t (source (Lf W (Vg (psE S) j) \1c)) by aw. rewrite !compfV // (LfV (hu _ jI)te). rewrite /W f_S' (LgV lij) (idV (set1_1 \0c)). rewrite LfV//; fprops; Wtac. move:(proj1 (prl_map2_prop pc pd)); case; rewrite (proj33(ex4d)). set v:= (projective_limit_fun S S' u) => [fv sv tv]. have nsv: ~ surjection v. by case;rewrite sv tv => _ h; move: (h _ ye) => [x /in_set0]. split => // i iI. rewrite /u LgV//; apply: lf_surjective; first by move => t _; apply: set1_1. rewrite I_S in iI. move:(ex4_setEi_nonempty (proj1 ex4d_orderIr_prop3) iI); rewrite {1} E_S. by move => [k ke] t/set1_P y0; exists k => //; rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)