proposition: Lemma urank_powerset a x : ordinalp a -> inc x (universe a) -> inc (\Po x) (universe (osucc a)) /\ (urank a (\Po x)) = osucc (urank a x).
proof: Proof. move => oa xa. move: (urank_pr1 oa xa); set r := urank a x; move => [ra pra]. move /oleSltP: ra => sra. have pa: sub (\Po x) (universe (osucc r)). move: pra => [uu vv _]; move => t /setP_P tcx; rewrite (universe_succ uu). apply /setP_P; apply: sub_trans tcx vv. move: (sub_trans pa (universe_inc2 sra)) => sa. split; first by rewrite (universe_succ oa); apply /setP_P. move: (urank_pr oa sa); move => [qa qb]. suff:urank_prop (\Po x) (osucc r) by move => h; apply(urank_uniq qb h). split => //; first exact: (proj31 sra). move => c /oltSleP cr h; move: (h _ (setP_Ti x))=> xc. move: (urank_pr1 (proj31 cr) xc) => [u1 u2]. by move: cr ; rewrite (urank_uniq pra u2) =>/(oltNge u1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)