proposition: Lemma OS_ordinal r: worder r -> ordinalp (ordinal r).
proof: Proof. move => wor. move => X ha hb. move: (proj1 wor)=> or. move: (transfinite_defined_pr target wor). set f := (transfinite_defined r target); move => [suf sf vf]. set E:= substrate r. have ff: function f by fct_tac. have H x: inc x E -> Vf f x = Vfs f (segment r x). by move /vf; rewrite /restriction1; aw. pose A := Zo E (fun z => inc (Vf f z) X). have Ha: segmentp r A. split;first by apply: Zo_S. move => x y xA lxy; case: (equal_or_not y x) => ltxy; first by ue. have yE: inc y E by rewrite /E; order_tac. move /Zo_P:xA => [xE fbX]; apply: (Zo_i yE); apply: (hb _ fbX). have ssf: sub (segment r x) (source f) by rewrite sf;apply: sub_segment. rewrite (H _ xE). by apply/(Vf_image_P ff ssf); exists y => //; apply /segmentP. have sas: sub A (source f) by rewrite sf; apply: Zo_S. have <-: Vfs f A = X. set_extens t; first by move/(Vf_image_P ff sas) =>[u /Zo_hi ua ->]. move => tX; apply/(Vf_image_P ff sas). move: (proj2 suf _ (ha _ tX)) =>[u usf eq1]; exists u => //. by apply: Zo_i; [rewrite /E - sf | ue]. case: (well_ordered_segment wor Ha). by move ->; rewrite /ordinal - (surjective_pr0 suf) - sf . by move =>[a aE ->] _;rewrite -(H a aE); apply: (Vf_target ff); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)