We will prove ∃alpha : set, ordinal alpha ∧ uncountable_set alpha.

We prove the intermediate claim Hex: ∃X : set, well_ordered_set X ∧ uncountable_set X ∧ countable_subsets_bounded X.

An exact proof term for the current goal is exists_uncountable_well_ordered_set.

Apply Hex to the current goal.

Let X be given.

Assume HX: well_ordered_set X ∧ uncountable_set X ∧ countable_subsets_bounded X.

We prove the intermediate claim HX0: well_ordered_set X ∧ uncountable_set X.

An exact proof term for the current goal is (andEL (well_ordered_set X ∧ uncountable_set X) (countable_subsets_bounded X) HX).

We prove the intermediate claim Hwo: well_ordered_set X.

An exact proof term for the current goal is (andEL (well_ordered_set X) (uncountable_set X) HX0).

We prove the intermediate claim HuncX: uncountable_set X.

An exact proof term for the current goal is (andER (well_ordered_set X) (uncountable_set X) HX0).

We use X to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (well_ordered_set_is_ordinal X Hwo).

An exact proof term for the current goal is HuncX.

∎