Theorem mirimanoff

Description: Mirimanoff's paradox: The class of grounded sets is not a set. Here, a set x is grounded if there is no infinite membership-descending sequence of sets beginning with x . See Paragraph 1 of Quine p. 37 . (Contributed by Adrian Ducourtial, 11-Oct-2026)

	Ref	Expression
Hypothesis	mirimanoff.1	$$⊢M=\left\{x|\neg \exists f\left(fFn\mathrm{\omega }\wedge f\left(\varnothing \right)=x\wedge \forall n\in \mathrm{\omega }f\left(\mathrm{suc}n\right)\in f\left(n\right)\right)\right\}$$
Assertion	mirimanoff	$$⊢M\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mirimanoff.1	$$⊢M=\left\{x|\neg \exists f\left(fFn\mathrm{\omega }\wedge f\left(\varnothing \right)=x\wedge \forall n\in \mathrm{\omega }f\left(\mathrm{suc}n\right)\in f\left(n\right)\right)\right\}$$
2		rabab	$$⊢\left\{x\in \mathrm{V}|\neg \exists f\left(fFn\mathrm{\omega }\wedge f\left(\varnothing \right)=x\wedge \forall n\in \mathrm{\omega }f\left(\mathrm{suc}n\right)\in f\left(n\right)\right)\right\}=\left\{x|\neg \exists f\left(fFn\mathrm{\omega }\wedge f\left(\varnothing \right)=x\wedge \forall n\in \mathrm{\omega }f\left(\mathrm{suc}n\right)\in f\left(n\right)\right)\right\}$$
3	1 2	eqtr4i	$$⊢M=\left\{x\in \mathrm{V}|\neg \exists f\left(fFn\mathrm{\omega }\wedge f\left(\varnothing \right)=x\wedge \forall n\in \mathrm{\omega }f\left(\mathrm{suc}n\right)\in f\left(n\right)\right)\right\}$$
4	3	mirimanoffr	$$⊢M\notin \mathrm{V}$$