English
For ordinals x,y, x ⊆ y iff x = y or x ∈ y.
Русский
Для ординалов x,y верно: x ⊆ y тогда либо x = y, либо x ∈ y.
LaTeX
$$$IsOrdinal(x) \land IsOrdinal(y) \Rightarrow (x \subseteq y \iff (x = y \lor x \in y))$$$
Lean4
theorem subset_iff_eq_or_mem (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y ↔ x = y ∨ x ∈ y :=
by
constructor
· revert hx hy
apply Sym2.GameAdd.induction mem_wf _ x y
intro x y IH hx hy hxy
by_cases hyx : y ⊆ x
· exact Or.inl (subset_antisymm hxy hyx)
· obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y.toSet \ x.toSet) (Set.diff_nonempty.2 hyx)
have hmy : m ∈ y := show m ∈ y.toSet from Set.mem_of_mem_diff hm
have hmx : m ⊆ x := by
intro z hzm
by_contra hzx
exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
· exact Or.inr hmy
· cases Set.notMem_of_mem_diff hm H
· rintro (rfl | h)
· rfl
· exact hy.subset_of_mem h
