proposition: Lemma Exercise6_33r n: inc n N0 -> [/\ sub alpha (source (y n)), inc (yr n) (functions alpha (unionf alpha Mi)) & forall i, inc i alpha -> Vf (y n) i = Vf (yr n) i].
proof: Proof. move => nN. move: Exercise6_33q => [sa _ _ sd se]. move: (sa _ nN) => [nc asy _ ]. move: (Exercise6_33j nc) => [ [_ _ [bjy _ _] _] sy ty]. have fy: function (y n) by fct_tac. have osy: ordinalp (source (y n)). rewrite sy; exact: (proj32_1 (proj32 (Exercise6_33i nc))). have Ha t: inc t alpha -> inc t (source (y n)). by move/ (oltP osy): asy => /proj1/proj33; apply. have ax: lf_axiom [eta Vf (y n)] alpha (unionf alpha Mi). move => t ta; move: (Ha t ta) => ts. move: (Vf_target fy ts); rewrite ty; move/ (Exercise6_33e nc) => qa. by apply/setUf_P; exists t => //; apply: Zo_i => //; exists n. rewrite /yr /E6_33_yr;split => //. by apply /functionsP; saw; apply: lf_function. by move => i ia; bw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)