proposition: Lemma transfinite_aux2 r T s (tdf: fterm) : worder r -> (alls s (segmentp r)) -> (forall z, inc z s -> transfiniteg_def (induced_order r z) T (tdf z)) -> let f := (unionf s tdf) in transfiniteg_def (induced_order r (union s)) T f.
proof: Proof. move=> wo alseg altd. set f := unionf s tdf. have or := proj1 wo. have prop1 y: inc y s -> substrate (induced_order r y) = y. move => /alseg h; apply:(iorder_sr or(sub_segment1 h)). have prop2 y: inc y s -> domain (tdf y) = y. by move => ys; rewrite (proj32 (altd _ ys)) (prop1 _ ys). have sgf: sgraph f by move => t /setUf_P [y /altd [[ha _] _ _] td]; apply: ha. have df: domain f = union s. set_extens t. move /(domainP sgf) => [y /setUf_P [z zs /domain_i]]. rewrite (prop2 _ zs) => tz; union_tac. move => /setU_P [y ty ys]; apply/(domainP sgf). move: ty; rewrite - (prop2 _ ys) => /(domainP (proj1 (proj31 (altd _ ys)))). move => [z za]; exists z; apply/setUf_P; ex_tac. have su: sub (union s) (substrate r). by move=> v /setU_hi [i vi /alseg /proj1]; apply. have sr1:= (iorder_sr or su). have hb0 i j x: inc i s -> inc j s -> inc x i -> inc x j -> sub i j -> Vg (tdf i) x = Vg (tdf j) x. move => ins jns xi xj sij. suff: (tdf i) = restr (tdf j) i by move ->; rewrite LgV. have seg1 := (alseg _ ins); have seg2 := (alseg _ jns). have sjr:= proj1 seg2. have sir:= sub_trans sij sjr. have iv: i = substrate (induced_order r i) by rewrite iorder_sr. have woi: worder (induced_order r i) by apply: induced_wor. apply: (transfiniteg_unique woi (altd i ins)). split;[apply: restr_fgraph | by rewrite restr_d | rewrite - iv => t ti]. have tj := (sij _ ti). move:(tj); rewrite - {1}(iorder_sr or sjr) => tsj. move:(altd j jns) => [ha hv hc]. rewrite (restr_ev _ ti) (hc _ tsj). rewrite (segment_induced_a seg2 tj). rewrite (segment_induced_a seg1 ti) double_restr //. by move => u /(lt_in_segment2 seg1 ti). have hb i j x: inc i s -> inc j s -> inc x i -> inc x j -> Vg (tdf i) x = Vg (tdf j) x. move=> ins jns x1 x2. move: (alseg _ ins) (alseg _ jns) (altd _ ins) (altd _ jns)=> si sj ti tj. case: (segment_dichot_sub wo si sj) => sij; first by apply: hb0. by symmetry; apply: hb0. have fgf: fgraph f. split => // x y /setUf_P [x' x's x'v] /setUf_P [y' y's y'v] eq. rewrite (in_graph_V (proj31 (altd _ x's)) x'v). rewrite (in_graph_V (proj31 (altd _ y's)) y'v) - eq (hb _ _ _ x's y's) //. by move:(domain_i1 x'v); rewrite prop2. by move:(domain_i1 y'v); rewrite eq prop2. have fv i x : inc x i -> inc i s -> Vg f x = Vg (tdf i) x. move => xi ins; suff: inc (J x (Vg (tdf i) x)) f by move/(pr2_V fgf); aw. move:(altd _ ins) => [g1 d1 _]. by apply/setUf_P; ex_tac; apply: (fdomain_pr1 g1); rewrite prop2. split => //; first by rewrite sr1 df. rewrite sr1 => x xu;move: (xu)=>/setU_P [i xi ins]; rewrite (fv _ _ xi ins). rewrite (proj33 (altd _ ins)) ?(prop1 _ ins) //; congr T. rewrite (segment_induced_a (alseg _ ins) xi). rewrite (segment_induced_a (setU_segment alseg) xu). apply: restr_exten => t /(lt_in_segment2 (alseg _ ins) xi) ti. by rewrite (fv _ _ ti ins). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)