proposition: Lemma Lemma5_02 : forall xi, xi < alpha -> phi xi gamma = gamma.
proof: Proof. intros xi Hxi. assert (forall n, phi xi (gamma_ n) <= gamma). { intro n; apply le_trans with (gamma_ (S n)). cbn; apply sup_upper_bound. generalize (@countable_image _ _ (members alpha) (fun x => phi x (gamma_ n))). intros H; apply countable_downward_closed with (image (members alpha) (fun x => phi x (gamma_ n))). apply H. apply countable_members. destruct 1. destruct H. apply countable_members. exists x0. split; auto. destruct H0; auto. destruct H0;auto. exists xi; split; auto. unfold gamma; apply sup_upper_bound. apply seq_range_countable. exists (S n); auto. } assert (sup (seq_range (fun n => phi xi (gamma_ n))) <= gamma). { apply sup_least_upper_bound. apply seq_range_countable. intros y [n [_ Hn]]. subst; apply H. } assert (phi xi gamma <= gamma). { unfold gamma at 1; unfold omega_limit. assert (continuous (phi xi) ordinal (Cr xi)). { apply Th_13_5_2. replace ordinal with (the_ordering_segment (Cr xi)). apply ord_ok. apply segment_unbounded. eapply ordering_function_seg with (Cr xi). exists (phi xi). apply ord_ok; auto. assert (Unbounded (Cr xi)) by(now destruct (IHalpha Hxi)). rewrite (@ ordering_unbounded_unbounded (A_ xi) (Cr xi) (phi xi)) in H1. auto. apply ord_ok. destruct (IHalpha Hxi); auto. } destruct H1. destruct H2. rewrite <- H3. - apply sup_least_upper_bound. apply countable_image. apply seq_range_countable. intros y [x [H4 H5]]. destruct H4 as [z [_ H6]]. subst x y; apply H. - split. - exists (gamma_ 0), 0;auto. - apply seq_range_countable. } assert (gamma <= phi xi gamma). { eapply ordering_le. - apply ord_ok. - assert (Unbounded (Cr xi)) by ( now destruct (IHalpha Hxi)). replace (the_ordering_segment (Cr xi)) with ordinal. + split. + rewrite (@ordering_unbounded_unbounded (A_ xi) (Cr xi) (phi xi)) in H2. * unfold A_ in H2; symmetry; apply segment_unbounded; auto. apply segment_the_ordering_segment; auto. * apply ord_ok. } apply le_antisym; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)