proposition: Lemma extensional_pr X: foundation_axiom -> extensional_set X -> exists! f, [/\ bijection f, source f = X, transitive_set(target f) & forall a b, inc a X -> inc b X -> (inc a b <-> inc (Vf f a) (Vf f b))].
proof: Proof. move => pa pb; apply/unique_existence; split; last first. move => f g [[[ff ijf] sjf] sf tf fp] [[[fg ijg] sjg] sg tg gp]. set A:= Zo X (fun a => Vf f a <> Vf g a). case: (pa A). move => ae;apply: function_exten4 => //;[ ue | move => a ax; ex_middle bad]. empty_tac1 a; apply:Zo_i => //; ue. move => [y /Zo_P [yX fgy] dya]; case: fgy. have sa: sub (y \cap X) (source f) by rewrite sf; apply:subsetI2r. have sb: sub (y \cap X) (source g) by rewrite sg; apply:subsetI2r. have ->: Vf f y = Vfs f (y \cap X). set_extens t. move => tvf; apply/(Vf_image_P ff sa). have vft: inc (Vf f y) (target f) by Wtac. move:(tf _ vft _ tvf) => /(proj2 sjf) [u usf uv]; exists u; try ue. rewrite sf in usf; apply/setI2_P; split => //. by apply/(fp u y usf yX); ue. by move/(Vf_image_P ff sa) => [u /setI2_P [uy uX] ->];apply/(fp u y uX yX). have ->: Vf g y = Vfs g (y \cap X). set_extens t. move => tvf; apply/(Vf_image_P fg sb). have vft: inc (Vf g y) (target g) by Wtac. move:(tg _ vft _ tvf) => /(proj2 sjg) [u usf uv]; exists u; try ue. rewrite sg in usf; apply/setI2_P; split => //. by apply/(gp u y usf yX); ue. by move/(Vf_image_P fg sb) => [u /setI2_P [uy uX] ->];apply/(gp u y uX yX). set_extens t. move/(Vf_image_P ff sa) => [u ua ->];apply/(Vf_image_P fg sb); ex_tac. by move/setI2_P: ua => [uy uX]; ex_middle bad; empty_tac1 u;apply:Zo_i. move/(Vf_image_P fg sb) => [u ua ->];apply/(Vf_image_P ff sa); ex_tac. symmetry. by move/setI2_P: ua => [uy uX]; ex_middle bad; empty_tac1 u;apply:Zo_i. pose W x := inc x X. have ha: (forall x, W x -> ordinalp (urank0 x)). by move => x wx; move:(urank0_pr2 pa x) => []. have hb: (forall i, ordinalp i -> exists E, forall x : Set, inc x E <-> W x /\ urank0 x <o i). move => i oi; exists (Zo X (fun z => urank0 z <o i)) => x; split. by move /Zo_P. by move => h; apply/Zo_P. pose H x f := Zo (range f) (fun z => exists2 t, inc t (x \cap X) & z = Vg f t). move: (stratified_fct_pr H ha hb) => Ha. set F:= stratified_fct W H urank0. have hd: forall x, inc x X -> F x = fun_image (x \cap X) F. move => x xX; rewrite /F (Ha _ xX) -/F. have ->: stratified_set W urank0 (urank0 x) = Zo X (fun t => urank0 t <o urank0 x). have oi:= ha _ xX. have hc:=(stratified_setP hb oi). set_extens t; [by move/hc=> hd; apply/Zo_P | by move/Zo_P/hc ]. rewrite /H; set_extens t. move => /Zo_P [/Lg_range_P [b /Zo_P [qa qb] ->] [v va ->]]. rewrite LgV; first by apply/funI_P; ex_tac. move/setI2_P: va => [vx vX]; apply:Zo_i => //. apply:(urank0_pr3 (AF_universe pa x) vx). move=>/funI_P [z /setI2_P [zx zX] ->]. have he: inc z (Zo X (fun u => urank0 u <o urank0 x)). by apply:Zo_i => //; apply:(urank0_pr3 (AF_universe pa x) zx). apply /Zo_P; split; first by apply/Lg_range_P;exists z => //; apply:Zo_i. exists z; [ by apply/setI2_P | rewrite LgV//]. have he: forall x, ordinalp x -> forall a b, inc a X -> inc b X -> (urank0 a) <o x -> (urank0 b) <o x -> F a = F b -> a = b. pose p x := forall a b : Set, inc a X -> inc b X -> urank0 a <o x -> urank0 b <o x -> F a = F b -> a = b. move => x ox; case:(least_ordinal6 p ox) => //. set alpha := least_ordinal _ _. move => [oa hrec]; case => a b ax bx h1 h2. rewrite (hd _ ax) (hd _ bx) => h; apply: (pb _ _ ax bx). have aux: forall u v, inc u (a \cap X) -> inc v (b \cap X) -> F u = F v -> u = v. move => u v /setI2_P [ua uX] /setI2_P [ub vX]. have ra:= (urank0_pr3 (AF_universe pa a) ua). have rb:= (urank0_pr3 (AF_universe pa b) ub). move:(proj31_1 h1)(proj31_1 h2) => o1 o2. set c:= Yo (urank0 a <=o urank0 b) (urank0 b) (urank0 a). have ca: (urank0 a) <=o c by rewrite /c; Ytac hu;fprops. have cb: (urank0 b) <=o c. rewrite /c; Ytac hu; fprops. by case: (oleT_el o2 o1) => // [][]. have cc: c <o alpha by rewrite /c; Ytac hu => //. have ica: inc c alpha by apply /(oltP oa). apply:((hrec _ ica) _ _ uX vX (olt_leT ra ca)(olt_leT rb cb)). set_extens t => ta. have: inc (F t) (fun_image (b \cap X) F) by rewrite -h ; apply/funI_P; ex_tac. move /funI_P => [z za zb]; have -> //: t = z by apply: aux. have: inc (F t) (fun_image (a \cap X) F). by rewrite h ; apply/funI_P; ex_tac. move /funI_P => [z za zb]; have <- //: z = t by apply: aux. have hf: forall a b, inc a X -> inc b X -> F a = F b -> a = b. move => a b aX bX. move:(ha _ aX) (ha _ bX) => oa ob. set c:= Yo (urank0 a <=o urank0 b) (urank0 b) (urank0 a). have ca: (urank0 a) <=o c by rewrite /c; Ytac hu; fprops. have cb: (urank0 b) <=o c. rewrite /c; Ytac hu; fprops. by case: (oleT_el ob oa) => // [][]. have sa:= (oltS (proj32 ca)). exact: (he _ (proj32_1 sa) _ _ aX bX (ole_ltT ca sa) (ole_ltT cb sa)). set T:= fun_image X F. have ax: forall a, inc a X -> inc (F a) T. move => a ax; apply/funI_P; ex_tac. set f := Lf F X T. exists f;split => //. + by apply: lf_bijective => // y /funI_P. + by rewrite /f; aw. + rewrite /f; aw; move => Y /funI_P [z zx]; rewrite (hd _ zx). move => -> t /funI_P [u /setI2_P [ua ub ->]]; apply/funI_P; ex_tac. + move => a b aX bX; rewrite /f !LfV// (hd _ bX); split. by move => ab; apply /funI_P; exists a=> //; apply/setI2_P. by move => /funI_P [z /setI2_P [za zx]] /(hf _ _ aX zx) ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)