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 = { x | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) }
Assertion	mirimanoff	|- M e/ _V

Proof

Step	Hyp	Ref	Expression
1		mirimanoff.1	|- M = { x | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) }
2		rabab	|- { x e. _V | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) } = { x | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) }
3	1 2	eqtr4i	|- M = { x e. _V | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) }
4	3	mirimanoffr	|- M e/ _V