proposition: Lemma CNFB_e_p7 x n (y := Vf (CNFB_expos_rec x) n): ordinalp x -> natp n -> (finite_set y /\ ordinal_set y).
proof: Proof. move=> ox; rewrite /y; clear y; move : n. move: (induction_defined_pr (fun z => union (fun_image z CNFB_expos)) (CNFB_expos x)). rewrite -/(CNFB_expos_rec x); move=> [sg sjg gz gnz]. apply: Nat_induction. rewrite gz. exact (CNFB_e_p2 ox). move => n nB [pa pb]; rewrite (gnz _ nB); split. rewrite - setUb_identity; apply: finite_union_finite. hnf;rewrite /identity_g; aw =>i idf; rewrite LgV//. move: idf => /funI_P [z zn ->]. by move: (CNFB_e_p2 (pb _ zn)) => [ok _]. by rewrite /identity_g; aw; apply: finite_fun_image. move=> t /setU_P [y ty] /funI_P [z zw yv]. move: (CNFB_e_p2 (pb _ zw)) => [_ ok]. by rewrite - yv in ok; apply: ok. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)