proposition: Lemma ordinals_set_iso E (p := inc ^~E) (r:= fun x y => [/\ p x, p y & x <=o y]) (A:= ordinal (ole_on E)): (ordinal_set E) -> (lf_axiom (ordinals r) A E) /\ order_isomorphism (Lf (ordinals r) A E) (ordinal_o A) (ole_on E).
proof: Proof. move => pa. move: (worder_rc_op p) ; rewrite -/r => pc. have ose: (forall a, inc a E -> a <=o a) by move => a /pa op; apply:oleR. have rxx: forall x, r x x <-> inc x E. move => x; split; [ by move =>[] | move => xE;split; fprops ]. pose H a := (exists2 x, r x x & a = ordinalr r x). have pd: forall a, H a -> (r (ordinals r a) (ordinals r a) /\ ordinalr r (ordinals r a) = a). by move => a ha; apply: ordinalsP. have pe: forall x, inc x E -> ordinals r (ordinalr r x) = x. by move => x /rxx xe;apply: ordinalsrP. move: (wordering_ole_pr pa) => [sc sd]. have ra: forall x, inc x E -> inc (ordinalr r x) A. move => x /rxx xE; suff: (ordinalr r x) <o A by move /oltP0 => []. move: (worder_rc_seg pc xE) => []; rewrite -/r => [sa sb]. move: (segmentrP (proj2 pc) xE); rewrite -/r => sp. apply: order_cp3 => //; first split. + apply /(order_cp0 (proj1 sa) (proj1 sc))=> u v. by move/graph_on_P1 => [_ _ uv];apply/graph_on_P1. + move => /(f_equal substrate); rewrite sb sd => ss. by move /rxx:(xE); rewrite - ss; move /sp => [_]. + hnf; rewrite sb sd;split; first by move =>t /sp [] []. move => u v /sp [[pu px ux] nux] /graph_on_P1 [ve _ vu]; apply /sp; split. split => //; apply:oleT vu ux. move => vx; case: nux; rewrite vx in vu; apply:oleA ux vu. have rb:forall a, inc a A -> H a. move => a aA. move: (the_ordinal_iso1 sc); rewrite -/A; set f:= the_ordinal_iso _. rewrite /order_isomorphism sd ordinal_o_sr. move => [sa sb [[[ff injf] [_ sjf]] sf tf] isf]. hnf in isf; rewrite sf in injf isf. set x := Vf f a. have xe: r x x by apply /rxx;rewrite - tf /x; Wtac. have [ta tb] :=(worder_rc_seg pc xe). have oA:ordinalp A by exact: (OS_ordinal sc). have oa :=(Os_ordinal oA aA). have saA :=(ordinal_transitive oA aA). exists x => //; symmetry;rewrite /ordinalr;apply: ordinal_o_isu2 => //. have la: lf_axiom (Vf f) a (segmentr r x). move => t ita; move: (saA _ ita) => tA. have [[_ _ lte] nta]: t <o a by apply /oltP. have: gle (ordinal_o A) t a by apply /sub_gleP. move /(isf _ _ tA aA) => /graph_on_P1. move => h; apply /(segmentrP (proj2 pc) xe); split => //. by move => hh; case: nta; apply/ (injf _ _ tA aA). apply:orderIS;exists (Lf (Vf f) a (segmentr r x)). hnf; rewrite tb ordinal_o_sr; split; fprops. hnf; saw; apply: lf_bijective => //. move => u v /saA ua /saA va; apply /(injf _ _ ua va). move => y /(segmentrP (proj2 pc) xe) [[yE _ rxy] xny]. rewrite tf in sjf;move: (sjf _ yE) => [];rewrite sf => [b bA bb]. case: (oleT_el (Os_ordinal oA aA) (Os_ordinal oA bA)). move => [_ _ ab]; have: gle (ordinal_o A) a b by apply /sub_gleP. move /(isf _ _ aA bA) => /graph_on_P1 [_ _];rewrite -bb - /x => xy. case: xny; apply:oleA rxy xy. move /(oltP oa) => ba; ex_tac. hnf;aw;move => u v ua va; rewrite !LfV//. move: (saA _ ua) (saA _ va) => uA vA; split. move/sub_gleP=> [_ _ h1]; have: gle (ordinal_o A) u v by apply /sub_gleP. move /(isf _ _ uA vA) => /graph_on_P1 [_ _ le]. apply/graph_on_P1; split;try apply: la => //; split => //; rewrite /p; Wtac. move /graph_on_P1 => [_ _ [_ _ le]]. have:(gle (ole_on E) (Vf f u) (Vf f v)). apply/graph_on_P1; split => //; Wtac. by move /(isf _ _ uA vA) => /sub_gleP [_ _ h1]; apply/sub_gleP. set fp := ordinals r. have rc: forall a, inc a A -> inc (fp a) E /\ ordinalr r (fp a) = a. by move => a /rb /pd [/rxx sa sb]. set f := Lf fp A E. have lfa: lf_axiom fp A E by move => t /rc []. have bf: bijection_prop f A E. hnf;rewrite /f; saw; apply: lf_bijective. - by exact. - by move => u v /rc [_ e1] /rc [_ e2] e3; rewrite - e1 - e2 e3. - by move => y yE; rewrite -(pe _ yE); move: (ra _ yE) => h; ex_tac. split => //. split => //; [ apply: ordinal_o_or | fprops | by rewrite ordinal_o_sr sd |]. hnf; rewrite /f; aw; move => x y xA yA; rewrite !LfV//. move: (rc _ xA) (rc _ yA) => [ta tb][tc td]; split => h. move:(proj2 (worder_total sc));rewrite sd => to;case: (to _ _ ta tc) => //hh. move /sub_gleP:h => [_ _ ce]. suff: x = y by move => h1; move: hh; rewrite h1. move/graph_on_P1:hh => /(ordinalr_Mle pc). by rewrite tb td; move => [_ _ cp]; apply: extensionality. move/graph_on_P1:h => /(ordinalr_Mle pc). by rewrite tb td; move => [_ _ cp];apply/sub_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)