Theorem mirimanofff

Description: Mirimanoff's paradox mirimanoff for founded sets. A set x is founded if every set containing x has a minimal element under membership. Compare with zfreg the defining condition of M in the hypothesis. (Contributed by Adrian Ducourtial, 28-Oct-2026)

	Ref	Expression
Hypothesis	mirimanofff.1	|- M = { x | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) }
Assertion	mirimanofff	|- M e/ _V

Proof

Step	Hyp	Ref	Expression
1		mirimanofff.1	|- M = { x | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) }
2		rabab	|- { x e. _V | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) } = { x | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) }
3	1 2	eqtr4i	|- M = { x e. _V | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) }
4	3	mirimanofffr	|- M e/ _V