English
The membership relation is well-founded on ZFSet: there are no infinite descending chains x1 ∈ x0, …; every nonempty set has a minimal element with respect to ∈.
Русский
Отношение принадлежности на ZFSet является хорошо основанным: не существует бесконечной нисходящей цепи x1 ∈ x0 ∈ x-1 …; у каждого непустого множества есть минимальный элемент по отношению к ∈.
LaTeX
$$$\\operatorname{WellFounded}(\\in)\\quad\\text{(mem_wf) on ZFSet}$$$
Lean4
theorem mem_wf : @WellFounded ZFSet (· ∈ ·) :=
(wellFounded_lift₂_iff (H := fun a b c d hx hy =>
propext ((@Mem.congr_left a c hx).trans (@Mem.congr_right b d hy _)))).mpr
PSet.mem_wf
