proposition: Theorem transfinite_definition_stable r T F: worder r -> (forall f, function f -> segmentp r (source f) -> sub (target f) F -> inc (T f) F) -> sub (target (transfinite_defined r T)) F.
proof: Proof. move => wor hb t. have or := proj1 wor. move:(transfinite_defined_pr T wor); set f := transfinite_defined r T. move => [[ff sfj] sf frec] /sfj [x xsf ->]; move: x xsf;rewrite sf. case: (worder_prop2 (fun x => inc (Vf f x) F) wor) => // - [x [xsr xa px]]. move: (frec _ xsr). have ssa: sub (segment r x) (source f) by rewrite sf; apply:sub_segment. move:(restriction1_fs ff ssa) => [fg]. move: (hb _ fg); rewrite [in (source _)] /restriction1; aw => p1 p2 => sa. have aux: sub (target (restriction1 f (segment r x))) F. move => y /p2 [u ua ->]. by rewrite (restriction1_V ff ssa ua); move /segmentP: ua => /px. by move: (p1 (segment_segment _ or) aux); rewrite - sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)