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