proposition: Lemma universe_rec z: ordinalp z -> universe z = unionf z (fun t => \Po (universe t)).
proof: Proof. move => oz. rewrite /universe. set p := (fun f => unionf (range f) powerset). rewrite (transdef_ord_pr p oz) {1}/p. set_extens t. move /setUf_P => [y /Lg_range_P [b bz ->] tp]; apply/setUf_P; ex_tac. move/setUf_P => [y yz tv]; apply/setUf_P. exists (transdef_ord p y) => //; apply/Lg_range_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)