Apply In_ind to the current goal.
Let alpha be given.
Assume IHalpha: ∀gamma ∈ alpha, ∀beta : set, ordinal gamma → ordinal beta → gamma ∈ beta ∨ gamma = beta ∨ beta ∈ gamma.
We will prove ∀beta : set, ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha.
Apply In_ind to the current goal.
Let beta be given.
Assume IHbeta: ∀delta ∈ beta, ordinal alpha → ordinal delta → alpha ∈ delta ∨ alpha = delta ∨ delta ∈ alpha.
Assume Halpha: ordinal alpha.
Assume Hbeta: ordinal beta.
We will prove alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha.
Apply (xm (alpha ∈ beta)) to the current goal.
Assume H1: alpha ∈ beta.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: alpha ∉ beta.
Apply (xm (beta ∈ alpha)) to the current goal.
Assume H2: beta ∈ alpha.
Apply or3I3 to the current goal.
An exact proof term for the current goal is H2.
Assume H2: beta ∉ alpha.
Apply or3I2 to the current goal.
We will prove alpha = beta.
Apply set_ext to the current goal.
We will prove alpha ⊆ beta.
Let gamma be given.
Assume H3: gamma ∈ alpha.
We will prove gamma ∈ beta.
We prove the intermediate claim Lgamma: ordinal gamma.
An exact proof term for the current goal is (ordinal_Hered alpha Halpha gamma H3).
Apply (or3E (gamma ∈ beta) (gamma = beta) (beta ∈ gamma) (IHalpha gamma H3 beta Lgamma Hbeta)) to the current goal.
Assume H4: gamma ∈ beta.
An exact proof term for the current goal is H4.
Assume H4: gamma = beta.
We will prove False.
Apply H2 to the current goal.
We will prove beta ∈ alpha.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3.
Assume H4: beta ∈ gamma.
We will prove False.
Apply H2 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is (ordinal_TransSet alpha Halpha gamma H3 beta H4).
We will prove beta ⊆ alpha.
Let delta be given.
Assume H3: delta ∈ beta.
We will prove delta ∈ alpha.
We prove the intermediate claim Ldelta: ordinal delta.
An exact proof term for the current goal is (ordinal_Hered beta Hbeta delta H3).
Apply (or3E (alpha ∈ delta) (alpha = delta) (delta ∈ alpha) (IHbeta delta H3 Halpha Ldelta)) to the current goal.
Assume H4: alpha ∈ delta.
We will prove False.
Apply H1 to the current goal.
We will prove alpha ∈ beta.
An exact proof term for the current goal is (ordinal_TransSet beta Hbeta delta H3 alpha H4).
Assume H4: alpha = delta.
We will prove False.
Apply H1 to the current goal.
We will prove alpha ∈ beta.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H3.
Assume H4: delta ∈ alpha.
An exact proof term for the current goal is H4.
∎