proposition: Lemma ex3_gl_val_bf (E := (projective_limit ex3limit_graphs)) (f:= Lf ex3_gl_val ex3_graphs_limit E): bijection_prop f ex3_graphs_limit E.
proof: Proof. have ax:= ex3_gl_val_ax. rewrite /f;saw. case:(prl_map2_prop same_I Hu); set fp := (projective_limit_fun S S' u). move => [fff sff tff] ffp. have huu i: inc i (psI S) -> function_prop (Vg u i) (Vg (psE S) i) (Vg (psE S') i). by move => iI; move:Hu => [_ _ h _]; move: (h _ iI). have hu i: inc i (psI S) -> function (Vg u i) by case /huu. apply: (lf_bijective ax). move => u1 u2 u1g u2g sv. rewrite (in_graph_Vf fff u1g) (in_graph_Vf fff u2g). suff : (P u1) = P u2 by move ->. move: (p1graph_source1 fff u1g) (p1graph_source1 fff u2g). rewrite sff. move => /prl_limitP [pu1g u1d u1v u1w]. move => /prl_limitP [pu2g u2d u2v u2w]. apply: fgraph_exten => //; first by rewrite u1d u2d. rewrite u1d => i iI. move: (f_equal (fun z => P (Vg z i)) sv);rewrite /ex3_gl_val. by rewrite !LgV//; aw. move => y yp. move:(prl_subsets_prop ex3_prl_subfm_hyp). rewrite -/ex3limit_graphs; move => [s_E s_I s_r s_f]. move:(yp) =>/prl_limitP[yg yd yv yw]. set x1 := (Lg (psI S) (fun i => (P (Vg y i)))). set x2 := (Lg (psI S) (fun i => (Q (Vg y i)))). have dy: domain (psE ex3limit_graphs) = psI S by rewrite s_E Lgd. rewrite s_E in yv. have xyv : y = ex3_gl_val (J x1 x2). rewrite /ex3_gl_val; apply:fgraph_exten; aww. rewrite /x1 /x2 yd => i iI; rewrite ! LgV//; aw. move:(hu _ iI) => fu. by move: (yv _ iI); rewrite LgV// => yig;rewrite (function_sgraph fu yig). have xsp: inc x1 (projective_limit S). apply/Zo_P; split. rewrite /x1; apply/setXb_P; rewrite ps_domain_E; split; aww. move => i iI; rewrite LgV//; move:(yv _ iI)(huu _ iI); rewrite LgV// => yv' [fu <- _]. exact: (p1graph_source1 fu yv'). move => i j lij. move:(prl_system_product_prop same_I) =>[s_E' s_I' s_r' s_f']. move: (prl_prop0 lij) => [iI jI]. move:(ps_function_f lij) => [fij sij _]. move:(lij); rewrite same_I => lij'. move:(ps_function_f lij') => [fij' sij' _]. move:(yv _ iI)(yv _ jI);rewrite /x1 !LgV// => yv1 yv2. move: (prl_subfam_prop1 ex3_prl_subfm_hyp) (yw _ _ lij)=> [_ Fb _ _ _]. move: (Fb _ _ (Vg y j) lij); rewrite LgV// => ww; move: (ww yv2)=> {Fb ww}. move => -> -> /=; rewrite /prl_product_f (LgV lij). rewrite (ext_to_prod_V2 fij fij') ?pr1_pair // sij sij'; aw. move: (huu _ jI) => [fuj <- <-]. rewrite - (function_sgraph fuj yv2); apply:setXp_i. - exact:(p1graph_source1 fuj yv2). - exact:(p2graph_target1 fuj yv2). move:(xsp); rewrite - sff => xsp'. have pqx: x2 = Vf fp x1. move:(Vf_target fff xsp'); rewrite tff => /prl_limitP[vg vd vv vw]. rewrite /x2; apply: fgraph_exten => //; aww. by rewrite vd (prl_same_index_same_I same_I). move => i iI /=. rewrite -(prl_map_val_aux2 same_I Hu iI xsp) /x1 LgV//. by move:(yv _ iI) (hu _ iI); rewrite ! LgV// => yv' fu; apply: Vf_pr2. by exists (J x1 x2) => //; rewrite pqx;apply:(Vf_pr3 fff xsp'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)